Further progress on right orthogonal calculus - part 2

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

@@ -409,6 +409,50 @@ from composition and cancelling laws for equivalences.
     ( ihc (f' a''))
     ( ihc'' a'')
 
+```
+
+We can cancel the left homotopy cartesian square if its lower map
+`f' : A'' → A'` has a section.
+
+```rzk
+#def is-homotopy-cartesian-left-cancel-with-lower-section
+  ( has-section-f' : has-section A'' A' f')
+  ( ihc' : is-homotopy-cartesian A'' C'' A' C' f' F')
+  ( ihc'' : is-homotopy-cartesian A'' C'' A C
+              ( comp A'' A' A f f')
+              ( \ a'' →
+                comp (C'' a'') (C' (f' a'')) (C (f (f' a'')))
+                  (F (f' a'')) (F' a'')))
+  : is-homotopy-cartesian A' C' A C f F
+  :=
+    ind-has-section A'' A' f' has-section-f'
+    ( \ a' → is-equiv (C' a') (C (f a')) (F a'))
+    ( \ a'' →
+      is-equiv-left-factor (C'' a'') (C' (f' a'')) (C (f (f' a'')))
+      ( F' a'') (ihc' a'')
+      ( F (f' a'')) ( ihc'' a''))
+```
+
+In fact, it suffices to assume that the left square has horizontal sections.
+
+```rzk
+#def is-homotopy-cartesian-left-cancel-with-section
+  ( has-section-f' : has-section A'' A' f')
+  ( has-sections-F' : (a'' : A'') → has-section (C'' a'') (C' (f' a'')) (F' a''))
+  ( ihc'' : is-homotopy-cartesian A'' C'' A C
+              ( comp A'' A' A f f')
+              ( \ a'' →
+                comp (C'' a'') (C' (f' a'')) (C (f (f' a'')))
+                  (F (f' a'')) (F' a'')))
+  : is-homotopy-cartesian A' C' A C f F
+  :=
+    ind-has-section A'' A' f' has-section-f'
+    ( \ a' → is-equiv (C' a') (C (f a')) (F a'))
+    ( \ a'' →
+      is-equiv-left-cancel (C'' a'') (C' (f' a'')) (C (f (f' a'')))
+      ( F' a'') ( has-sections-F' a'')
+      ( F (f' a'')) ( ihc'' a''))
+
 #end homotopy-cartesian-horizontal-calculus
 ```
 

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

@@ -704,6 +704,7 @@ We now assume extension extensionality and derive a few consequences.
 
 ```rzk
 #assume extext : ExtExt
+#assume naiveextext : NaiveExtExt
 ```
 
 In particular, extension extensionality implies that homotopies give rise to
@@ -722,6 +723,8 @@ retraction to `#!rzk ext-htpy-eq`.
   := first (first (extext I ψ ϕ A a f g))
 ```
 
+### Functoriality properties of extension types
+
 By extension extensionality, fiberwise equivalences of extension types define
 equivalences of extension types. For simplicity, we extend from `#!rzk BOT`.
 
@@ -760,6 +763,28 @@ equivalences of extension types. For simplicity, we extend from `#!rzk BOT`.
               ( \ t → second (second (second (famequiv t))) (b t))))))
 ```
 
+Similarly, a fiberwise section of a map `(t : ψ) → A t → B t` induces a section
+on extension types
+
+```rzk
+#def has-section-extension-has-section-family uses (naiveextext)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( A B : ψ → U)
+  ( f : ( t : ψ) → A t → B t)
+  ( has-fiberwise-section-f : (t : ψ) → has-section (A t ) (B t) (f t))
+  : has-section ((t : ψ) → A t) ((t : ψ) → B t) ( \ a t → f t (a t))
+  :=
+    ( ( \ b t → first (has-fiberwise-section-f t) (b t))
+    , \ b →
+      ( naiveextext I ψ (\ _ → BOT) B (\ _ → recBOT)
+        ( \ t → f t (first (has-fiberwise-section-f t) (b t)))
+        ( \ t → b t)
+        ( \ t → second (has-fiberwise-section-f t) (b t))))
+```
+
+### Homotopy extension property
+
 We have a homotopy extension property.
 
 The following code is another instantiation of casting, necessary for some

src/simplicial-hott/04-right-orthogonal.rzk.md

@@ -8,11 +8,13 @@ This is a literate `rzk` file:
 
 ## Prerequisites
 
-Some of the definitions in this file rely on extension extensionality:
+Some of the definitions in this file rely on extension extensionality or
+function extensionality:
 
 ```rzk
 #assume naiveextext : NaiveExtExt
 #assume extext : ExtExt
+#assume funext : FunExt
 #assume weakextext : WeakExtExt
 ```
 
@@ -380,6 +382,51 @@ stability properties of maps right orthogonal to it.
 #variable ϕ : ψ → TOPE
 ```
 
+### Equivalences are right orthogonal
+
+Every equivalence `α : A' → A` is right orthogonal to `ϕ ⊂ ψ`.
+
+```rzk
+#def is-right-orthogonal-is-equiv-to-shape uses (extext)
+  ( A' A : U)
+  ( α : A' → A)
+  ( is-equiv-α : is-equiv A' A α)
+  : is-right-orthogonal-to-shape I ψ ϕ A' A α
+  :=
+    is-homotopy-cartesian-is-horizontal-equiv
+      ( ϕ → A') (\ σ' → (t : ψ) → A' [ϕ t ↦ σ' t])
+      ( ϕ → A) (\ σ → (t : ψ) → A [ϕ t ↦ σ t])
+      ( \ σ' t → α (σ' t))
+      ( \ _ τ' t → α (τ' t))
+      ( second
+        ( equiv-extension-equiv-family extext I ( \ t → ϕ t)
+          ( \ _ → A') ( \ _ → A) ( \ _ → (α , is-equiv-α))))
+     ( is-equiv-Equiv-is-equiv'
+         ( ψ → A') ( ψ → A) ( \ τ' t → α (τ' t))
+         ( Σ (σ' : ϕ → A') , (t : ψ) → A' [ϕ t ↦ σ' t])
+         ( Σ (σ : ϕ → A) , (t : ψ) → A [ϕ t ↦ σ t])
+         ( \ (σ' , τ') → ( \ t → α (σ' t) , \ t → α (τ' t)))
+       ( cofibration-composition-functorial I ψ ϕ ( \ _ → BOT)
+           ( \ _ → A') ( \ _ → A) ( \ _ → α) ( \ _ → recBOT))
+       ( second
+         ( equiv-extension-equiv-family extext I ( \ t → ψ t)
+           ( \ _ → A') ( \ _ → A) ( \ _ → (α , is-equiv-α)))))
+```
+
+Right orthogonality is closed under homotopy.
+
+```rzk
+#def is-right-orthogonal-homotopy-to-shape uses (funext)
+  ( A' A : U)
+  ( α β : A' → A)
+  ( h : homotopy A' A α β)
+  : is-right-orthogonal-to-shape I ψ ϕ A' A α
+  → is-right-orthogonal-to-shape I ψ ϕ A' A β
+  :=
+    transport (A' → A) ( is-right-orthogonal-to-shape I ψ ϕ A' A) α β
+    ( first (first (funext A' (\ _ → A) α β)) h)
+```
+
 ### Stability under composition
 
 ```rzk
@@ -416,13 +463,36 @@ stability properties of maps right orthogonal to it.
   :=
     \ σ'' →
     is-equiv-right-factor
-      ( extension-type I ψ ϕ (\ _ → A'') σ'')
-      ( extension-type I ψ ϕ (\ _ → A') (\ t → α' (σ'' t)))
-      ( extension-type I ψ ϕ (\ _ → A) (\ t → α (α' (σ'' t))))
-      ( \ τ'' t → α' (τ'' t))
-      ( \ τ' t → α (τ' t))
-      ( is-orth-ψ-ϕ-α (\ t → α' (σ'' t)))
-      ( is-orth-ψ-ϕ-αα' σ'')
+     ( extension-type I ψ ϕ (\ _ → A'') σ'')
+     ( extension-type I ψ ϕ (\ _ → A') (\ t → α' (σ'' t)))
+     ( extension-type I ψ ϕ (\ _ → A) (\ t → α (α' (σ'' t))))
+     ( \ τ'' t → α' (τ'' t))
+     ( \ τ' t → α (τ' t))
+     ( is-orth-ψ-ϕ-α (\ t → α' (σ'' t)))
+     ( is-orth-ψ-ϕ-αα' σ'')
+```
+
+### Left cancellation with section (weak version)
+
+This should hold even without assuming `is-orth-ψ-ϕ-α'`.
+
+```rzk
+#def is-right-orthogonal-weak-left-cancel-with-section-to-shape
+      uses (naiveextext is-orth-ψ-ϕ-α' is-orth-ψ-ϕ-αα')
+  ( has-section-α' : has-section A'' A' α')
+  : is-right-orthogonal-to-shape I ψ ϕ A' A α
+  :=
+    is-homotopy-cartesian-left-cancel-with-lower-section
+        ( ϕ → A'' ) ( \ σ'' → (t : ψ) → A'' [ϕ t ↦ σ'' t])
+        ( ϕ → A' ) ( \ σ' → (t : ψ) → A' [ϕ t ↦ σ' t])
+        ( ϕ → A ) ( \ σ → (t : ψ) → A [ϕ t ↦ σ t])
+        ( \ σ'' t → α' (σ'' t)) ( \ _ τ'' x → α' (τ'' x) )
+        ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) )
+    ( has-section-extension-has-section-family naiveextext I (\ t → ϕ t)
+          ( \ _ → A'') (\ _ → A') (\ _ → α')
+      ( \ _ → has-section-α'))
+    ( is-orth-ψ-ϕ-α')
+    ( is-orth-ψ-ϕ-αα')
 ```
 
 ### Stability under pullback
@@ -580,6 +650,55 @@ Then we can deduce that right orthogonal maps are preserved under pullback:
 #end right-orthogonal-calculus
 ```
 
+### Right orthogonal maps are closed under equivalence
+
+If two maps `α : A' → A` and `β : B' → B` are equivalent, then if one is right
+orthogonal to `ϕ ⊂ ψ`, then so is the other.
+
+```rzk
+#section is-right-orthogonal-equiv-to-shape
+
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+#variables A' A : U
+#variable α : A' → A
+#variables B' B : U
+#variable β : B' → B
+
+#def is-right-orthogonal-equiv-to-shape uses (funext extext)
+  ( (((s', s), η), (is-equiv-s', is-equiv-s)) : Equiv-of-maps A' A α B' B β)
+  ( is-orth-ψ-ϕ-β : is-right-orthogonal-to-shape I ψ ϕ B' B β)
+  : is-right-orthogonal-to-shape I ψ ϕ A' A α
+  :=
+    is-right-orthogonal-right-cancel-to-shape I ψ ϕ A' A B α s
+    ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A B s is-equiv-s)
+    ( is-right-orthogonal-homotopy-to-shape I ψ ϕ A' B
+      ( \ a' → β (s' a')) ( \ a' → s (α a')) ( η)
+      ( is-right-orthogonal-comp-to-shape I ψ ϕ A' B' B s' β
+        ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A' B' s' is-equiv-s')
+        ( is-orth-ψ-ϕ-β)))
+
+#def is-right-orthogonal-equiv-to-shape'
+  uses (funext extext naiveextext)
+  ( (((s', s), η), (is-equiv-s', is-equiv-s)) : Equiv-of-maps A' A α B' B β)
+  ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)
+  : is-right-orthogonal-to-shape I ψ ϕ B' B β
+  :=
+    is-right-orthogonal-weak-left-cancel-with-section-to-shape
+          I ψ ϕ A' B' B s' β
+    ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A' B' s' is-equiv-s')
+    ( is-right-orthogonal-homotopy-to-shape I ψ ϕ A' B
+      ( \ a' → s (α a')) ( \ a' → β (s' a'))
+      ( rev-homotopy A' B ( \ a' → β (s' a')) ( \ a' → s (α a')) ( η))
+      ( is-right-orthogonal-comp-to-shape I ψ ϕ A' A B α s
+        ( is-orth-ψ-ϕ-α)
+        ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A B s is-equiv-s)))
+    ( second is-equiv-s')
+
+#end is-right-orthogonal-equiv-to-shape
+```
+
 ## Types with unique extension
 
 We say that an type `A` has unique extensions for a shape inclusion `ϕ ⊂ ψ`, if