Functorial isomorphism of shape inclusions

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

@@ -472,6 +472,118 @@ In fact, it suffices to assume that the left square has horizontal sections.
 #end homotopy-cartesian-horizontal-calculus
 ```
 
+### Homotopy cartesian faces of a cube
+
+Consider two squares induced by type families as follows
+
+```rzk
+#section is-homotopy-cartesian-in-cube
+
+#variable A' : U
+#variable C' : A' → U
+#variable A : U
+#variable C : A → U
+#variable α : A' → A
+#variable γ : (a' : A') → C' a' → C (α a')
+
+#variable B' : U
+#variable D' : B' → U
+#variable B : U
+#variable D : B → U
+#variable β : B' → B
+#variable δ : (b' : B') → D' b' → D (β b')
+```
+
+and a map between them in the following strict sense
+
+```rzk
+#variable f' : A' → B'
+#variable f : A → B
+#variable h : (a' : A') → β (f' a') = f (α a')
+
+#variable F' : (a' : A') → C' a' → D' (f' a')
+#variable F : (a : A) → C a → D (f a)
+#variable H
+  : (a' : A')
+  → (c' : C' a')
+  → ( transport B D (β (f' a')) (f (α a')) (h a')
+      ( δ (f' a') (F' a' c'))
+    = F (α a') (γ a' c'))
+```
+
+We view this as a cube
+
+```
+      Σ D'      Σ D
+
+Σ C'      Σ C
+
+       B'        B
+
+ A'        A
+```
+
+with display maps going down and ordinary maps going to the right and up-right.
+
+Assume furthermore that the two squares on the left and right are themselves
+homotopy cartesian.
+
+```rzk
+#variable is-hc-CD' : is-homotopy-cartesian A' C' B' D' f' F'
+#variable is-hc-CD : is-homotopy-cartesian A C B D f F
+```
+
+If the square `B' D' B D` is homotopy cartesian, then so is `A' C' A C`.
+
+```rzk
+#def is-homotopy-cartesian-in-cube
+  : is-homotopy-cartesian B' D' B D β δ
+  → is-homotopy-cartesian A' C' A C α γ
+  :=
+  \ is-hc-BD a' →
+    is-equiv-equiv-is-equiv
+    ( C' a') (C (α a')) (γ a')
+    ( D' (f' a')) (D (f (α a')))
+    (\ d' → transport B D (β (f' a')) (f (α a')) (h a') (δ (f' a') d'))
+    ( ( F' a' ,  F (α a')) , H a')
+    ( is-hc-CD' a')
+    ( is-hc-CD (α a'))
+    ( is-equiv-comp
+      ( D' (f' a')) (D (β (f' a'))) (D (f (α a')))
+      ( δ (f' a')) (is-hc-BD (f' a'))
+      ( transport B D (β (f' a')) (f (α a')) (h a'))
+      ( is-equiv-transport B D (β (f' a')) (f (α a')) (h a')))
+```
+
+The converse holds provided that the map `f' : A' → B'` has a section.
+
+```rzk
+#def is-homotopy-cartesian-in-cube'
+  ( has-sec-f' : has-section A' B' f')
+  : is-homotopy-cartesian A' C' A C α γ
+  → is-homotopy-cartesian B' D' B D β δ
+  :=
+  \ is-hc-AC →
+    ind-has-section A' B' f' has-sec-f'
+    ( \ b' → is-equiv (D' b') (D (β b')) (δ b'))
+    ( \ a' →
+      ( is-equiv-right-factor
+        ( D' (f' a')) (D (β (f' a'))) (D (f (α a')))
+        ( δ (f' a'))
+        ( transport B D (β (f' a')) (f (α a')) (h a'))
+        ( is-equiv-transport B D (β (f' a')) (f (α a')) (h a'))
+        ( is-equiv-equiv-is-equiv'
+          ( C' a') (C (α a')) (γ a')
+          ( D' (f' a')) (D (f (α a')))
+          (\ d' → transport B D (β (f' a')) (f (α a')) (h a') (δ (f' a') d'))
+          ( ( F' a' ,  F (α a')) , H a')
+          ( is-hc-CD' a')
+          ( is-hc-CD (α a'))
+          ( is-hc-AC a'))))
+
+#end is-homotopy-cartesian-in-cube
+```
+
 ## Fiber products
 
 Given two type families `B C : A → U`, we can form their **fiberwise product**.

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

@@ -334,3 +334,109 @@ to diagrams extending a fixed diagram `σ': ϕ → A'` (or, respectively, its im
     , \ τ' → second (is-fretract-ψ-χ A' A α) τ'
     )
 ```
+
+### Isomorphisms of shape inclusions
+
+Consider two shape inclusions `ϕ ⊂ ψ` and `ζ ⊂ χ`. We want to express the fact
+that there is an isomorphism `ψ ≅ χ` of shapes which restricts to an isomorphism
+`ϕ ≅ ζ`. Since shapes are not types themselves, the best we can currently do is
+describe this isomorphism on representables.
+
+```rzk
+#def isomorphism-shape-inclusions
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  : U
+  :=
+    ( Σ ( f : (A : U) → Equiv (ζ → A) (ϕ → A))
+      , ( ( A : U)
+        → ( σ : ζ → A)
+        → ( Equiv
+            ( (t : χ) → A [ζ t ↦ σ t])
+            ( (t : ψ) → A [ϕ t ↦ first (f A) σ t]))))
+
+#def functorial-isomorphism-shape-inclusions
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  : U
+  :=
+  Σ ( (f , F) : isomorphism-shape-inclusions I ψ ϕ J χ ζ)
+  , ( Σ ( e
+          : ( A' : U)
+          → ( A : U)
+          → ( α : A' → A)
+          → ( σ' : ζ → A')
+          → ( ( \ (t : I | ϕ t) → α (first (f A') σ' t))
+            = ( first (f A) (\ t → α (σ' t)))))
+      , ( ( A' : U)
+        → ( A : U)
+        → ( α : A' → A)
+        → ( σ' : ζ → A')
+        → ( τ' : (t : χ) → A' [ζ t ↦ σ' t])
+        → ( ( transport (ϕ → A) (\ σ → (t : ψ) → A [ϕ t ↦ σ t])
+              ( \ (t : I | ϕ t) → α (first (f A') σ' t))
+              ( first (f A) (\ t → α (σ' t)))
+              ( e A' A α σ')
+              (\ (t : ψ) → α (first (F A' σ') τ' t)))
+            = ( first (F A (\ (t : ζ) → α (σ' t))) (\ (t : χ) → α (τ' t))))))
+```
+
+In practice, the isomorphisms are usually given via an explicit formula, which
+would define a map `ψ → ϕ` if `ψ` and `ϕ` were themselves types. In this case
+all the coherences are just `refl`, hence it is easy to produce a term of type
+`functorial-isomorphism-shape-inclusions I ψ ϕ J χ ζ`.
+
+For example, consider the two shape inclusions `{0} ⊂ Δ¹` (subshapes of `2`) and
+`{1} ⊂ right-leg-of-Λ` (subshapes of `2 × 2`), where
+
+```rzk
+#def right-leg-of-Λ : Λ → TOPE
+  := \ (t, s) → t ≡ 1₂
+```
+
+These two shape inclusions are canonically isomorphic via the formulas
+
+```
+-- not valid rzk code
+#def f : Δ¹ → right-leg-of-Λ
+  \ s → (1₂ , s)
+
+#def g : right-leg-of-Λ → Δ¹
+  \ (t , s) → s
+```
+
+We turn these formulas into a functorial shape inclusion as follows.
+Unfortunately we have to repeat the same formula multiple times, leading to some
+ugly boilerplate code.
+
+```rzk
+#def isomorphism-0-Δ¹-1-right-leg-of-Λ
+  : isomorphism-shape-inclusions
+    (2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)
+    2 Δ¹ (\ t → t ≡ 0₂)
+  :=
+    ( \ A →
+      ( \ τ (t,s) → τ s
+      , ( ( \ υ s → υ (1₂, s) , \ _ → refl)
+        , ( \ υ s → υ (1₂, s) , \ _ → refl)))
+    , \ A _ →
+      ( \ τ (t,s) → τ s
+      , ( ( \ υ s → υ (1₂, s) , \ _ → refl)
+        , ( \ υ s → υ (1₂, s) , \ _ → refl))))
+
+#def functorial-isomorphism-0-Δ¹-1-right-leg-of-Λ
+  : functorial-isomorphism-shape-inclusions
+    (2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)
+    2 Δ¹ (\ t → t ≡ 0₂)
+  :=
+    ( isomorphism-0-Δ¹-1-right-leg-of-Λ
+    , ( \ _ _ _ _ → refl , \ _ _ _ _ _ → refl))
+```

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

@@ -192,7 +192,7 @@ occasionally go back or forth along the functorial equivalence
       ( is-orth-ψ-ϕ σ'))
 ```
 
-### Stability under composition
+### Composition
 
 Left orthogonal shape inclusions are preserved under composition.
 
@@ -228,7 +228,7 @@ Left orthogonal shape inclusions are preserved under composition.
           σ')
 ```
 
-### Cancellation laws
+### Cancellation
 
 If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so is `χ ⊂ ψ`.
 
@@ -318,7 +318,7 @@ affecting left orthogonality.
     ( is-orth-ψ-ϕ (\ (s , t) → σ' (t , s)))
 ```
 
-### Stability under exponentiation
+### Exponentiation
 
 If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` then so is `χ × ϕ ⊂ χ × ψ` for
 every other shape `χ`.
@@ -401,7 +401,7 @@ extensionality.
     ( is-right-orthogonal-to-shape-product A' A α J χ I ψ ϕ is-orth-ψ-ϕ)
 ```
 
-### Stability under exact pushouts
+### Exact pushouts
 
 For any two shapes `ϕ, ψ ⊂ I`, if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to
 `α : A' → A`, then so is `ψ ⊂ ϕ ∪ ψ`.
@@ -481,6 +481,70 @@ stability under pushout products.
       ( is-orth-ψ-ϕ))
 ```
 
+### Functorial isomorphisms of shape inclusion
+
+If two pairs of shape inclusions `ϕ ⊂ ψ` and `ζ ⊂ χ` are isomorphic, then
+`ϕ ⊂ ψ` is left orthogonal if and only if `ζ ⊂ χ` is left orthogonal.
+
+```rzk
+#def is-right-orthogonal-to-shape-isomorphism'
+  ( A' A : U)
+  ( α : A' → A)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  ( ((f , F) , (e , E)) : functorial-isomorphism-shape-inclusions I ψ ϕ J χ ζ)
+  : is-right-orthogonal-to-shape I ψ ϕ A' A α
+  →  is-right-orthogonal-to-shape J χ ζ A' A α
+  :=
+  is-homotopy-cartesian-in-cube
+  ( ζ → A') (\ σ' → (t : χ) → A' [ζ t ↦ σ' t])
+  ( ζ → A) (\ σ' → (t : χ) → A [ζ t ↦ σ' t])
+  ( \ σ' t → α (σ' t))
+  ( \ _ τ' t → α (τ' t))
+  ( ϕ → A') (\ σ' → (t : ψ) → A' [ϕ t ↦ σ' t])
+  ( ϕ → A) (\ σ' → (t : ψ) → A [ϕ t ↦ σ' t])
+  ( \ σ' t → α (σ' t))
+  ( \ _ τ' t → α (τ' t))
+  ( first (f A')) ( first (f A))
+  ( e A' A α)
+  ( \ σ' → first (F A' σ')) (\ σ → first (F A σ))
+  ( E A' A α)
+  ( \ σ' → second (F A' σ')) (\ σ → second (F A σ))
+
+#def is-right-orthogonal-to-shape-isomorphism
+  ( A' A : U)
+  ( α : A' → A)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  ( ((f , F) , (e , E)) : functorial-isomorphism-shape-inclusions I ψ ϕ J χ ζ)
+  : is-right-orthogonal-to-shape J χ ζ A' A α
+  → is-right-orthogonal-to-shape I ψ ϕ A' A α
+  :=
+  is-homotopy-cartesian-in-cube'
+  ( ζ → A') (\ σ' → (t : χ) → A' [ζ t ↦ σ' t])
+  ( ζ → A) (\ σ' → (t : χ) → A [ζ t ↦ σ' t])
+  ( \ σ' t → α (σ' t))
+  ( \ _ τ' t → α (τ' t))
+  ( ϕ → A') (\ σ' → (t : ψ) → A' [ϕ t ↦ σ' t])
+  ( ϕ → A) (\ σ' → (t : ψ) → A [ϕ t ↦ σ' t])
+  ( \ σ' t → α (σ' t))
+  ( \ _ τ' t → α (τ' t))
+  ( first (f A')) ( first (f A))
+  ( e A' A α)
+  ( \ σ' → first (F A' σ')) (\ σ → first (F A σ))
+  ( E A' A α)
+  ( \ σ' → second (F A' σ')) (\ σ → second (F A σ))
+  ( second (second (f A')))
+```
+
 ## Stability properties of right orthogonal maps
 
 Now we change perspective. We fix a shape inclusion `ϕ ⊂ ψ` and investigate
@@ -522,7 +586,7 @@ Right orthogonality is closed under homotopy.
     ( first (first (funext A' (\ _ → A) α β)) h)
 ```
 
-### Stability under composition
+### Composition
 
 ```rzk
 #variables A'' A' A : U
@@ -595,7 +659,7 @@ right (whether it is right orthogonal or not.)
     ( is-orth-ψ-ϕ-αα')
 ```
 
-### Stability under pullback
+### Pullback
 
 Right orthogonal maps are stable under pullback. More precisely: If `α : A' → A`
 is right orthogonal, then so is the second projection

src/simplicial-hott/08-covariant.rzk.md

@@ -309,8 +309,6 @@ The first step is to identify the pair `{0} ⊂ Δ¹` with the pair of subshapes
 `{1} ⊂ right-leg-of-Λ` of `Λ`.
 
 ```rzk
-#def right-leg-of-Λ : Λ → TOPE
-  := \ (t, s) → t ≡ 1₂
 
 #def is-equiv-Δ¹-to-right-leg-of-Λ-rel-start
   ( B : U)