Right orthogonal fibrations

src/hott/03-equivalences.rzk.md

@@ -739,6 +739,19 @@ dependent function types.
     Σ ( ( s',s) : product ( A' → B' ) ( A → B)),
       ( ( a' : A') → β ( s' a') = s ( α a'))
 
+#def Equiv-of-maps
+  ( A' A : U)
+  ( α : A' → A)
+  ( B' B : U)
+  ( β : B' → B)
+  : U
+  :=
+    Σ ( ((s', s), _) : map-of-maps A' A α B' B β),
+      ( product
+          ( is-equiv A' B' s')
+          ( is-equiv A B s)
+      )
+
 #def is-equiv-equiv-is-equiv
   ( A' A : U)
   ( α : A' → A)
@@ -758,6 +771,16 @@ dependent function types.
           ( is-equiv-comp A' B' B s' is-equiv-s' β is-equiv-β)
       )
 
+#def is-equiv-Equiv-is-equiv
+  ( A' A : U)
+  ( α : A' → A)
+  ( B' B : U)
+  ( β : B' → B)
+  ( ( S, (is-equiv-s',is-equiv-s)) : Equiv-of-maps A' A α B' B β )
+  : is-equiv B' B β → is-equiv A' A α
+  :=
+    is-equiv-equiv-is-equiv A' A α B' B β S is-equiv-s' is-equiv-s
+
 #def is-equiv-equiv-is-equiv'
   ( A' A : U)
   ( α : A' → A)
@@ -776,4 +799,14 @@ dependent function types.
         ( η)
         ( is-equiv-comp A' A B α is-equiv-α s is-equiv-s)
       )
+
+#def is-equiv-Equiv-is-equiv'
+  ( A' A : U)
+  ( α : A' → A)
+  ( B' B : U)
+  ( β : B' → B)
+  ( ( S, (is-equiv-s',is-equiv-s)) : Equiv-of-maps A' A α B' B β )
+  : is-equiv A' A α → is-equiv B' B β
+  :=
+    is-equiv-equiv-is-equiv' A' A α B' B β S is-equiv-s' is-equiv-s
 ```

src/hott/11-homotopy-pullbacks.rzk.md

@@ -314,20 +314,38 @@ the corresponding statements about equivalences established above.
         ( is-homotopy-cartesian-upper-to-fibers is-hc-γ-δ a')
         ( is-hc-α-γ a' )
 
-#def is-homotopy-cartesian-lower-cancellation
+#def is-homotopy-cartesian-vertical-pasting-from-fibers
+  ( is-hc-α-γ : is-homotopy-cartesian A' C' A C α γ )
+  ( is-fiberwise-hc-γ-δ
+    : ( a' : A') →
+      is-homotopy-cartesian (C' a') (D' a') (C (α a')) (D (α a')) (γ a') (δ a'))
+  : is-homotopy-cartesian-vertical-pasted
+  :=
+    is-homotopy-cartesian-vertical-pasting
+      is-hc-α-γ
+      ( is-homotopy-cartesian-upper-from-fibers is-fiberwise-hc-γ-δ)
+
+#def is-homotopy-cartesian-lower-cancel-to-fibers
+  ( is-hc-α-γ : is-homotopy-cartesian A' C' A C α γ )
+  ( is-hc-α-δ : is-homotopy-cartesian-vertical-pasted)
+  ( a' : A')
+  : is-homotopy-cartesian (C' a') (D' a') (C (α a')) (D (α a')) (γ a') (δ a')
+  :=
+    is-homotopy-cartesian-is-horizontal-equiv
+      ( C' a') (D' a') (C (α a')) (D (α a')) (γ a') (δ a')
+      ( is-hc-α-γ a')
+      ( is-hc-α-δ a')
+
+#def is-homotopy-cartesian-lower-cancel uses (D D' δ)
   ( is-hc-α-γ : is-homotopy-cartesian A' C' A C α γ )
   ( is-hc-α-δ : is-homotopy-cartesian-vertical-pasted
   )
   : is-homotopy-cartesian-upper
   :=
     is-homotopy-cartesian-upper-from-fibers
-    ( \ a' →
-        is-homotopy-cartesian-is-horizontal-equiv
-        ( C' a') (D' a') (C (α a')) (D (α a')) (γ a') (δ a')
-        ( is-hc-α-γ a')
-        ( is-hc-α-δ a'))
+      (is-homotopy-cartesian-lower-cancel-to-fibers is-hc-α-γ is-hc-α-δ)
 
-#def is-homotopy-cartesian-upper-cancellation-with-section
+#def is-homotopy-cartesian-upper-cancel-with-section
   ( has-sec-γ-δ : (a' : A') →
       has-section-family-over-map
         (C' a') (D' a') (C (α a')) (D (α a')) (γ a') (δ a'))
@@ -376,7 +394,7 @@ from composition and cancelling laws for equivalences.
       (F' a'') (ihc' a'')
       (F (f' a'')) (ihc (f' a''))
 
-#def is-homotopy-cartesian-right-cancellation
+#def is-homotopy-cartesian-right-cancel
   ( ihc : is-homotopy-cartesian A' C' A C f F)
   ( ihc'' : is-homotopy-cartesian A'' C'' A C
               ( comp A'' A' A f f')

src/simplicial-hott/03-simplicial-type-theory.rzk.md

@@ -178,6 +178,36 @@ For example, this applies to `Δ² ⊂ Δ¹×Δ¹`.
           \ a' → refl)
 ```
 
+Every functorial shape retract automatically induces a section
+when restricting to diagrams extending a fixed diagram `σ': ϕ → A'`
+(or, respectively, its image `ϕ → A` under α).
+
+```rzk
+#def relativize-is-functorial-shape-retract
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( χ : ψ → TOPE)
+  ( is-fretract-ψ-χ : is-functorial-shape-retract I ψ χ)
+  ( ϕ : χ → TOPE)
+  ( A' A : U)
+  ( α : A' → A)
+  ( σ' : ϕ → A')
+  : has-section-family-over-map
+      ( (t : χ) → A' [ϕ t ↦ σ' t])
+      ( \ τ' → (t : ψ) → A' [χ t ↦ τ' t])
+      ( (t : χ) → A [ϕ t ↦ α (σ' t)])
+      ( \ τ → (t : ψ) → A [χ t ↦ τ t])
+      ( \ τ' t → α (τ' t))
+      ( \ _ υ' t → α (υ' t))
+  :=
+    ( ( \ τ' → first (first (is-fretract-ψ-χ A' A α)) τ'
+      , \ τ → second (first (is-fretract-ψ-χ A' A α)) τ
+      )
+    , \ τ' → second (is-fretract-ψ-χ A' A α) τ'
+    )
+
+```
+
 ### Pushout product
 
 Pushout product Φ×ζ ∪\_{Φ×χ} ψ×χ of Φ ↪ ψ and χ ↪ ζ, domain of the co-gap map.
@@ -210,7 +240,7 @@ The intersection of shapes is defined by conjunction on topes.
 The union of shapes is defined by disjunction on topes.
 
 ```rzk
-#def shapeUnion
+#def shape-union
   ( I : CUBE)
   ( ψ χ : I → TOPE)
   : I → TOPE

src/simplicial-hott/04-extension-types.rzk.md

@@ -162,6 +162,31 @@ The original form.
     ( \ h → (\ t → h t , \ t → h t) ,
       ( ( \ (_f , g) t → g t , \ h → refl) ,
         ( ( \ (_f , g) t → g t , \ h → refl))))
+
+#def cofibration-composition-functorial
+  ( I : CUBE)
+  ( χ : I → TOPE)
+  ( ψ : χ → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A' A : χ → U)
+  ( α : (t : χ) → A' t → A t)
+  ( σ' : (t : ϕ) → A' t)
+  : Equiv-of-maps
+     ( (t : χ) → A' t [ϕ t ↦ σ' t])
+     ( (t : χ) → A t [ϕ t ↦ α t (σ' t)])
+     ( \ τ' t → α t (τ' t))
+     ( Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) ,
+        ( (t : χ) → A' t [ψ t ↦ τ' t]))
+     ( Σ ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) ,
+        ( (t : χ) → A t [ψ t ↦ τ t]))
+     ( \ (τ', υ') → ( \ t → α t (τ' t), \t → α t (υ' t)))
+  :=
+    ( ( ( \ h → (\ t → h t , \ t → h t) , \ h → (\ t → h t , \ t → h t)),
+        \ _ → refl),
+      ( ( ( \ (_f , g) t → g t , \ h → refl) ,
+          ( ( \ (_f , g) t → g t , \ h → refl))),
+        ( ( \ (_f , g) t → g t , \ h → refl) ,
+          ( ( \ (_f , g) t → g t , \ h → refl)))))
 ```
 
 A reformulated version via tope disjunction instead of inclusion (see
@@ -196,6 +221,31 @@ A reformulated version via tope disjunction instead of inclusion (see
     (\ h t → h t ,
       ( ( \ g t → recOR (ϕ t ↦ g t , ψ t ↦ a t) , \ _ → refl) ,
         ( \ g t → recOR (ϕ t ↦ g t , ψ t ↦ a t) , \ _ → refl)))
+
+#def cofibration-union-functorial
+  ( I : CUBE)
+  ( ϕ ψ : I → TOPE)
+  ( A' A : (t : I | ϕ t ∨ ψ t) → U)
+  ( α : (t : I | ϕ t ∨ ψ t) → A' t → A t)
+  ( τ' : (t : ψ) → A' t)
+  : Equiv-of-maps
+      ( (t : I | ϕ t ∨ ψ t) → A' t [ψ t ↦ τ' t])
+      ( (t : I | ϕ t ∨ ψ t) → A t [ψ t ↦ α t (τ' t)])
+      ( \ υ' t → α t (υ' t))
+      ( (t : ϕ) → A' t [ϕ t ∧ ψ t ↦ τ' t])
+      ( (t : ϕ) → A t [ϕ t ∧ ψ t ↦ α t (τ' t)])
+      ( \ ν' t → α t (ν' t))
+  :=
+     ( ( ( \ υ' t → υ' t
+         , \ υ t → υ t
+         )
+       , \ _ → refl
+       )
+     , ( second (cofibration-union I ϕ ψ A' τ')
+       ,
+         second (cofibration-union I ϕ ψ A ( \ t → α t (τ' t)))
+       )
+     )
 ```
 
 ## Extension extensionality
@@ -352,7 +402,7 @@ cases an extension type to a function type.
       ( ϕ )
       ( A )
       ( \ t y → (ext-projection-temp) t = y)
-      ( a ) -- a
+      ( a )
       ( \t → refl ))
     ( is-contr-ext-based-paths)
 
@@ -640,7 +690,7 @@ Both directions of this statement will be needed.
           rev
             ( A t )
             ( first (is-contr-fiberwise-A t) )
-            ( a t) --
+            ( a t)
             ( second (is-contr-fiberwise-A t) (a t))
 
 ```