resolve conflicts

mkdocs.yml

@@ -27,7 +27,7 @@ nav:
   - Simplicial HoTT:
       - Simplicial Type Theory: simplicial-hott/02-simplicial-type-theory.rzk.md
       - Extension Types: simplicial-hott/03-extension-types.rzk.md
-      - Right Orthogonal Fibrations: right-orthogonal/04-right-orthogonal.rzk.md
+      - Right Orthogonal Fibrations: simplicial-hott/04-right-orthogonal.rzk.md
       - Segal Types: simplicial-hott/05-segal-types.rzk.md
       - 2-Category of Segal Types: simplicial-hott/06-2cat-of-segal-types.rzk.md
       - Discrete Types: simplicial-hott/07-discrete.rzk.md

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

@@ -298,7 +298,7 @@ for a section of the family of extensions of a function `ϕ → A` to a function
 For example, this applies to `Δ² ⊂ Δ¹×Δ¹`.
 
 ```rzk
-#def Δ²-is-functorial-retract-Δ¹×Δ¹
+#def is-functorial-retract-Δ²-Δ¹×Δ¹
   : is-functorial-shape-retract (2 × 2) (Δ¹×Δ¹) (Δ²)
   :=
     \ A' A α →
@@ -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))
+```