Further progress on right orthogonal calculus

src/hott/03-equivalences.rzk.md

@@ -24,18 +24,6 @@ This is a literate `rzk` file:
   := Σ (r : B → A) , (homotopy A A (comp A B A r f) (identity A))
 ```
 
-```rzk
-#def ind-has-section
-  ( f : A → B)
-  ( ( sec-f , ε-f) : has-section f)
-  ( C : B → U)
-  ( s : ( a : A) → C ( f a))
-  ( b : B)
-  : C b
-  :=
-    transport B C ( f (sec-f b)) b ( ε-f b) ( s (sec-f b))
-```
-
 We define equivalences to be bi-invertible maps.
 
 ```rzk
@@ -70,9 +58,17 @@ We define equivalences to be bi-invertible maps.
   : B → A
   := first (second is-equiv-f)
 
+#def has-section-is-equiv
+  : has-section A B f
+  := second is-equiv-f
+
 #def retraction-is-equiv uses (f)
   : B → A
   := first (first is-equiv-f)
+
+#def has-retraction-is-equiv
+  : has-retraction A B f
+  := first is-equiv-f
 ```
 
 ```rzk title="The homotopy between the section and retraction of an equivalence"
@@ -214,7 +210,7 @@ The inverse of an invertible map has an inverse.
         first ( second has-inverse-f)))
 ```
 
-## Composing equivalences
+## The type of equivalences
 
 The type of equivalences between types uses `#!rzk is-equiv` rather than
 `#!rzk has-inverse`.
@@ -226,6 +222,34 @@ The type of equivalences between types uses `#!rzk is-equiv` rather than
   := Σ (f : A → B) , (is-equiv A B f)
 ```
 
+## Induction with section
+
+```rzk
+#def ind-has-section
+  ( A B : U)
+  ( f : A → B)
+  ( ( sec-f , ε-f) : has-section A B f)
+  ( C : B → U)
+  ( s : ( a : A) → C ( f a))
+  ( b : B)
+  : C b
+  :=
+    transport B C ( f (sec-f b)) b ( ε-f b) ( s (sec-f b))
+```
+
+It is convenient to have available the special case where `f` is an equivalence.
+
+```rzk
+#def ind-has-section-equiv
+  ( A B : U)
+  ( (f, is-equiv-f) : Equiv A B)
+  : ( C : B → U) → (( a : A) → C ( f a)) → ( b : B) → C b
+  :=
+    ind-has-section A B f (second is-equiv-f)
+```
+
+## Composing equivalences
+
 The data of an equivalence is not symmetric so we promote an equivalence to an
 invertible map to prove symmetry:
 
@@ -688,6 +712,16 @@ dependent function types.
   := (rev A x y , ((rev A y x , rev-rev A x y) , (rev A y x , rev-rev A y x)))
 ```
 
+```rzk
+#def ind-rev
+  ( A : U)
+  ( x y : A)
+  ( B : (x = y) → U)
+  : ((p : y = x) → B (rev A y x p)) → ( q : x = y) → B q
+  :=
+    ind-has-section-equiv (y = x) (x = y) (equiv-rev A y x) ( B)
+```
+
 ## Concatenation with a fixed path is an equivalence
 
 ```rzk

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

@@ -48,7 +48,7 @@ restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of
   :=
     \ τ → ( τ, refl)
 
-#def extension-type-weakening-section
+#def section-extension-type-weakening'
   : ( σ : (t : ϕ) → A t)
   → ( th : homotopy-extension-type σ)
   → Σ (τ : extension-type σ), (( τ, refl) =_{homotopy-extension-type σ} th)
@@ -63,17 +63,24 @@ restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of
   ( σ : (t : ϕ) → A t)
   : (homotopy-extension-type σ) → (extension-type σ)
   :=
-    \ th → first (extension-type-weakening-section σ th)
+    \ th → first (section-extension-type-weakening' σ th)
+
+#def has-section-extension-type-weakening
+  ( σ : (t : ϕ) → A t)
+  : has-section (extension-type σ) (homotopy-extension-type σ)
+      (extension-type-weakening-map σ)
+  :=
+    ( extension-strictification σ,
+      \ th → ( second (section-extension-type-weakening' σ th)))
+
 
 #def is-equiv-extension-type-weakening
   ( σ : (t : ϕ) → A t)
   : is-equiv (extension-type σ) (homotopy-extension-type σ)
       (extension-type-weakening-map σ)
   :=
-    ( ( extension-strictification σ ,
-        \ _ → refl),
-      ( extension-strictification σ,
-        \ th → ( second (extension-type-weakening-section σ th))))
+    ( ( extension-strictification σ, \ _ → refl)
+    , has-section-extension-type-weakening σ)
 
 #def extension-type-weakening
   ( σ : (t : ϕ) → A t)
@@ -116,7 +123,6 @@ This equivalence is functorial in the following sense:
       , is-equiv-extension-type-weakening I ψ ϕ A (\ t → α t (σ' t))
       )
     )
-
 ```
 
 ## Commutation of arguments and currying
@@ -1057,3 +1063,191 @@ $\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\r
         ( a)
         ( f))))
 ```
+
+### Pointwise homotopy extension types
+
+Using `ExtExt` we can write the homotopy in the homotopy extension type
+pointwise.
+
+```rzk
+#section pointwise-homotopy-extension-type
+
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+#variable A : ψ → U
+
+#def pointwise-homotopy-extension-type
+  ( σ : (t : ϕ) → A t)
+  : U
+  :=
+    Σ ( τ : (t : ψ) → A t) , ( (t : ϕ) → (τ t =_{ A t} σ t))
+
+#def equiv-pointwise-homotopy-extension-type uses (extext)
+  ( σ : (t : ϕ) → A t)
+  : Equiv
+    ( homotopy-extension-type I ψ ϕ A σ)
+    ( pointwise-homotopy-extension-type σ)
+  :=
+    total-equiv-family-equiv
+    ( (t : ψ) → A t)
+    ( \ τ → (\ t → τ t) =_{ (t : ϕ) → A t} σ)
+    ( \ τ → (t : ϕ) → (τ t = σ t))
+    ( \ τ →
+      equiv-ExtExt extext I (\ t → ϕ t) (\ _ → BOT) (\ t → A t)
+      ( \ _ → recBOT) ( \ t → τ t) ( σ))
+
+#def extension-type-pointwise-weakening uses (extext)
+  ( σ : (t : ϕ) → A t)
+  : Equiv
+    ( extension-type I ψ ϕ A σ)
+    ( pointwise-homotopy-extension-type σ)
+  := equiv-comp
+    ( extension-type I ψ ϕ A σ)
+    ( homotopy-extension-type I ψ ϕ A σ)
+    ( pointwise-homotopy-extension-type σ)
+    ( extension-type-weakening I ψ ϕ A σ)
+    ( equiv-pointwise-homotopy-extension-type σ)
+
+
+#end pointwise-homotopy-extension-type
+```
+
+## Relative extension types
+
+Given a map `α : A' → A`, there is also a notion of relative extension types.
+
+```rzk
+#section relative-extension-types
+
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+#variables A' A : ψ → U
+#variable α : (t : ψ) → A' t → A t
+#variable σ' : (t : ϕ) → A' t
+#variable τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]
+
+#def relative-extension-type
+  : U
+  :=
+    Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t])
+    , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl]
+
+#def relative-extension-type'
+  : U
+  :=
+    fib
+    ( (t : ψ) → A' t [ϕ t ↦ σ' t])
+    ( (t : ψ) → A t [ϕ t ↦ α t (σ' t)])
+    ( \ τ' t → α t (τ' t))
+    ( τ)
+
+#def equiv-relative-extension-type-fib uses (extext)
+  : Equiv
+    ( relative-extension-type')
+    ( relative-extension-type)
+  :=
+    total-equiv-family-equiv
+    ( (t : ψ) → A' t [ϕ t ↦ σ' t])
+    ( \ τ' → (\ t → α t (τ' t)) =_{ (t : ψ) → A t [ϕ t ↦ α t (σ' t)]} τ)
+    ( \ τ' → (t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl])
+    ( \ τ' →
+      equiv-ExtExt extext I ψ ϕ A (\ t → α t (σ' t))
+        ( \ t → α t (τ' t)) ( τ))
+#end relative-extension-types
+```
+
+### Generalized relative extension types
+
+We will also need to allow more general relative extension types, where we start
+with a `τ : ψ → A` that does not strictly restrict to `\ t → α (σ' t)`.
+
+```rzk
+#section general-extension-types
+
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+#variables A' A : ψ → U
+#variable α : (t : ψ) → A' t → A t
+
+#def general-relative-extension-type
+  ( σ' : (t : ϕ) → A' t)
+  ( τ : (t : ψ) → A t)
+  ( h : (t : ϕ) → α t (σ' t) = τ t)
+  : U
+  :=
+    Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t])
+    , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ h t]
+```
+
+If all ordinary relative extension types are contractible, then also all
+generalized ones.
+
+```rzk
+#def has-contr-relative-extension-types
+  : U
+  :=
+    ( σ' : (t : ϕ) → A' t)
+  → ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)])
+  → ( is-contr (relative-extension-type I ψ ϕ A' A α σ' τ))
+
+#def has-contr-general-relative-extension-types
+  : U
+  :=
+    ( σ' : (t : ϕ) → A' t)
+  → ( τ : (t : ψ) → A t)
+  → ( h : (t : ϕ) → α t (σ' t) = τ t)
+  → ( is-contr ( general-relative-extension-type σ' τ h))
+
+#def has-contr-relative-extension-types-generalize' uses (extext)
+  ( has-contr-relext-α : has-contr-relative-extension-types)
+  ( σ' : (t : ϕ) → A' t)
+  ( τ : (t : ψ) → A t)
+  ( h : (t : ϕ) → α t (σ' t) = τ t)
+  : is-contr
+    ( general-relative-extension-type σ' τ
+      ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t))))
+  :=
+    ind-has-section-equiv
+    ( extension-type I ψ ϕ A (\ t → α t (σ' t)))
+    ( pointwise-homotopy-extension-type I ψ ϕ A (\ t → α t (σ' t)))
+    ( extension-type-pointwise-weakening I ψ ϕ A (\ t → α t (σ' t)))
+    ( \ (τ̂ , ĥ) →
+      is-contr
+      ( general-relative-extension-type σ' τ̂
+        ( \ t → rev (A t) (τ̂ t) (α t (σ' t)) (ĥ t))))
+    ( \ τ → has-contr-relext-α σ' τ)
+    ( τ , \ t → (rev (A t) (α t (σ' t)) (τ t) (h t)))
+
+#def has-contr-relative-extension-types-generalize uses (extext)
+  ( has-contr-relext-α : has-contr-relative-extension-types)
+  : has-contr-general-relative-extension-types
+  :=
+  \ σ' τ h →
+    transport
+    ( (t : ϕ) → α t (σ' t) = τ t)
+    ( \ ĥ → is-contr ( general-relative-extension-type σ' τ ĥ))
+    ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t)))
+    ( h)
+    ( naiveextext-extext extext
+      ( I) (\ t → ϕ t) (\ _ → BOT) (\ t → α t (σ' t ) = τ t) (\ _ → recBOT)
+      ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t)))
+      ( h)
+      ( \ t → rev-rev (A t) (α t (σ' t)) (τ t) (h t)))
+    ( has-contr-relative-extension-types-generalize'
+         has-contr-relext-α σ' τ h)
+```
+
+The converse is of course trivial.
+
+```rzk
+#def has-contr-relative-extension-types-specialize
+  ( has-contr-gen-relext-α : has-contr-general-relative-extension-types)
+  :  has-contr-relative-extension-types
+  :=
+    \ σ' τ → has-contr-gen-relext-α σ' τ (\ _ → refl)
+
+#end general-extension-types
+```