From 3c078c5ff37af85ca0f675c13cdc36bfd02f6637 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@w199-8-v4.eduroam.dynamic.rbg.tum.de>
Date: Wed, 11 Oct 2023 12:10:22 +0200
Subject: [PATCH 01/10] restructure section and add
 is-right-orthogonal-to-shape-terminal-map

---
 .../04-right-orthogonal.rzk.md                | 87 +++++++++++--------
 1 file changed, 51 insertions(+), 36 deletions(-)

diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index 802fb1a4..f5de05b9 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -280,7 +280,8 @@ and relies on (the naive form of) extension extensionality.
 
 ### Stability under exact pushouts
 
-For any two shapes `ϕ, ψ ⊂ I`, if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to `α : A' → A`,
+For any two shapes `ϕ, ψ ⊂ I`,
+if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to `α : A' → A`,
 then so is `ψ ⊂ ϕ ∪ ψ`.
 
 ```rzk
@@ -309,60 +310,49 @@ We say that an type `A` has unique extensions for a shape inclusion `ϕ ⊂ ψ`,
 if for each `σ : ϕ → A` the type of `ψ`-extensions is contractible.
 
 ```rzk
+#section has-unique-extensions
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+#variable A : U
+
 #def has-unique-extensions
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( ϕ : ψ → TOPE)
-  ( A : U)
   : U
   :=
     ( σ : ϕ → A) → is-contr ( (t : ψ) → A [ϕ t ↦ σ t])
 ```
 
-The property of having unique extension
-can be pulled back along any right orthogonal map.
+There are a other equivalent characterizations:
+
+We can ask that the canonical restriction map `(ψ → A) → (ϕ → A)` is an
+equivalence.
 
 ```rzk
-#def has-unique-extensions-domain-right-orthogonal-has-unique-extensions-codomain
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( ϕ : ψ → TOPE)
-  ( A' A : U)
-  ( α : A' → A)
-  ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)
-  : has-unique-extensions I ψ ϕ A → has-unique-extensions I ψ ϕ A'
+#def is-local-type
+  : U
   :=
-    \ has-ue-A ( σ' : ϕ → A') →
-      is-contr-equiv-is-contr'
-        ( ( t : ψ) → A' [ϕ t ↦ σ' t])
-        ( ( t : ψ) → A [ϕ t ↦ α (σ' t)])
-        ( \ τ' t → α (τ' t) , is-orth-ψ-ϕ-α σ')
-        ( has-ue-A (\ t → α (σ' t)))
+    is-equiv (ψ → A) (ϕ → A) ( \ τ t → τ t)
 ```
 
-Alternatively, we can ask that the canonical restriction map `(ψ → A) → (ϕ → A)`
-is an equivalence.
+We can ask that the terminal map `A → Unit` is right orthogonal to `ϕ ⊂ ψ`
 
 ```rzk
-#section is-local-type
-#variable I : CUBE
-#variable ψ : I → TOPE
-#variable ϕ : ψ → TOPE
-#variable A : U
-
-#def is-local-type
+#def is-right-orthognal-to-shape-terminal-map
   : U
   :=
-    is-equiv (ψ → A) (ϕ → A) ( \ τ t → τ t)
+    is-right-orthogonal-to-shape I ψ ϕ A Unit (terminal-map A)
 ```
 
-This follows straightforwardly from the fact that for every `σ : ϕ → A`
+### Alternative characteriztions: proofs
+
+The equivalence between `is-local-type` and `has-unique-extensions` follows
+straightforwardly from the fact that for every `σ : ϕ → A`
 we have an equivalence between the extension type `(t : ψ) → A [ϕ t ↦ σ t]`
 and the fiber of the restriction map `(ψ → A) → (ϕ → A)`.
 
 ```rzk
 #def is-local-type-has-unique-extensions
-  ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A)
+  ( has-ue-ψ-ϕ-A : has-unique-extensions)
   : is-local-type
   :=
     is-equiv-is-contr-map (ψ → A) (ϕ → A) ( \ τ t → τ t)
@@ -375,7 +365,7 @@ and the fiber of the restriction map `(ψ → A) → (ϕ → A)`.
 
 #def has-unique-extensions-is-local-type
   ( is-lt-ψ-ϕ-A : is-local-type)
-  : has-unique-extensions I ψ ϕ A
+  : has-unique-extensions
   :=
     \ σ →
       is-contr-equiv-is-contr'
@@ -386,7 +376,33 @@ and the fiber of the restriction map `(ψ → A) → (ϕ → A)`.
             ( ψ → A) (ϕ → A) ( \ τ t → τ t)
             ( is-lt-ψ-ϕ-A)
             ( σ))
-#end is-local-type
+
+#end has-unique-extensions
+```
+
+
+
+### Stability properties of local types
+
+The property of having unique extension
+can be pulled back along any right orthogonal map.
+
+```rzk
+#def has-unique-extensions-domain-right-orthogonal-has-unique-extensions-codomain
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A' A : U)
+  ( α : A' → A)
+  ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)
+  : has-unique-extensions I ψ ϕ A → has-unique-extensions I ψ ϕ A'
+  :=
+    \ has-ue-A ( σ' : ϕ → A') →
+      is-contr-equiv-is-contr'
+        ( ( t : ψ) → A' [ϕ t ↦ σ' t])
+        ( ( t : ψ) → A [ϕ t ↦ α (σ' t)])
+        ( \ τ' t → α (τ' t) , is-orth-ψ-ϕ-α σ')
+        ( has-ue-A (\ t → α (σ' t)))
 ```
 
 Since the property of having unique extensions passes from the codomain to the domain
@@ -407,5 +423,4 @@ of a right orthogonal map, the same is true for locality of types.
       ( has-unique-extensions-domain-right-orthogonal-has-unique-extensions-codomain
           I ψ ϕ A' A α is-orth-α
           ( has-unique-extensions-is-local-type I ψ ϕ A is-local-A))
-
 ```

From 4cd42794271d4cbf329faa3fd7e478fe4f95fbd3 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Wed, 11 Oct 2023 14:21:21 +0200
Subject: [PATCH 02/10] local types = terminal map is right orthogonal

---
 .../04-right-orthogonal.rzk.md                | 143 +++++++++++++++---
 src/simplicial-hott/08-covariant.rzk.md       |   2 +-
 2 files changed, 123 insertions(+), 22 deletions(-)

diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index f5de05b9..8e86174b 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -8,10 +8,11 @@ This is a literate `rzk` file:
 
 ## Prerequisites
 
-Some of the definitions in this file rely on naive extension extensionality:
+Some of the definitions in this file rely on extension extensionality:
 
 ```rzk
 #assume naiveextext : NaiveExtExt
+#assume weakextext : WeakExtExt
 ```
 
 ## Right orthogonal maps with respect to shapes
@@ -322,7 +323,7 @@ if for each `σ : ϕ → A` the type of `ψ`-extensions is contractible.
     ( σ : ϕ → A) → is-contr ( (t : ψ) → A [ϕ t ↦ σ t])
 ```
 
-There are a other equivalent characterizations:
+There are a other equivalent characterizations which we shall prove below:
 
 We can ask that the canonical restriction map `(ψ → A) → (ϕ → A)` is an
 equivalence.
@@ -337,13 +338,13 @@ equivalence.
 We can ask that the terminal map `A → Unit` is right orthogonal to `ϕ ⊂ ψ`
 
 ```rzk
-#def is-right-orthognal-to-shape-terminal-map
+#def is-right-orthogonal-to-shape-terminal-map
   : U
   :=
     is-right-orthogonal-to-shape I ψ ϕ A Unit (terminal-map A)
 ```
 
-### Alternative characteriztions: proofs
+### Proof of first alternative characterization
 
 The equivalence between `is-local-type` and `has-unique-extensions` follows
 straightforwardly from the fact that for every `σ : ϕ → A`
@@ -381,17 +382,53 @@ and the fiber of the restriction map `(ψ → A) → (ϕ → A)`.
 ```
 
 
+### Properties of local types / unique extension types
 
-### Stability properties of local types
+We fix a shape inclusion `ϕ ⊂ ψ`.
 
-The property of having unique extension
+```rzk
+#section stability-properties-local-types
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+```
+
+Every map between types with unique extensions / local types
+is right orthogonal.
+
+```rzk
+#def is-right-orthogonal-have-unique-extensions
+  ( A' A : U)
+  ( has-ue-ψ-ϕ-A' : has-unique-extensions I ψ ϕ A')
+  ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A)
+  ( α : A' → A)
+  : is-right-orthogonal-to-shape I ψ ϕ A' A α
+  :=
+    \ σ →
+      is-equiv-are-contr
+      ( extension-type I ψ ϕ (\ _ → A') (σ))
+      ( extension-type I ψ ϕ (\ _ → A) (\ t → α (σ t)))
+      ( has-ue-ψ-ϕ-A' σ)
+      ( has-ue-ψ-ϕ-A (\ t → α (σ t)))
+      ( \ τ t → α (τ t))
+
+#def is-right-orthogonal-are-local-types
+  ( A' A : U)
+  ( is-lt-ψ-ϕ-A' : is-local-type I ψ ϕ A')
+  ( is-lt-ψ-ϕ-A : is-local-type I ψ ϕ A)
+  : ( α : A' → A)
+  → is-right-orthogonal-to-shape I ψ ϕ A' A α
+  :=
+    is-right-orthogonal-have-unique-extensions A' A
+    ( has-unique-extensions-is-local-type I ψ ϕ A' is-lt-ψ-ϕ-A')
+    ( has-unique-extensions-is-local-type I ψ ϕ A is-lt-ψ-ϕ-A)
+```
+
+Conversely, the property of having unique extension
 can be pulled back along any right orthogonal map.
 
 ```rzk
-#def has-unique-extensions-domain-right-orthogonal-has-unique-extensions-codomain
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( ϕ : ψ → TOPE)
+#def has-unique-extensions-right-orthogonal-has-unique-extensions
   ( A' A : U)
   ( α : A' → A)
   ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)
@@ -403,16 +440,8 @@ can be pulled back along any right orthogonal map.
         ( ( t : ψ) → A [ϕ t ↦ α (σ' t)])
         ( \ τ' t → α (τ' t) , is-orth-ψ-ϕ-α σ')
         ( has-ue-A (\ t → α (σ' t)))
-```
-
-Since the property of having unique extensions passes from the codomain to the domain
-of a right orthogonal map, the same is true for locality of types.
 
-```rzk
-#def is-local-type-domain-right-orthogonal-is-local-type-codomain
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( ϕ : ψ → TOPE)
+#def is-local-type-right-orthogonal-is-local-type
   ( A' A : U)
   ( α : A' → A)
   ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)
@@ -420,7 +449,79 @@ of a right orthogonal map, the same is true for locality of types.
   : is-local-type I ψ ϕ A'
   :=
     is-local-type-has-unique-extensions I ψ ϕ A'
-      ( has-unique-extensions-domain-right-orthogonal-has-unique-extensions-codomain
-          I ψ ϕ A' A α is-orth-α
+      ( has-unique-extensions-right-orthogonal-has-unique-extensions
+          ( A') ( A) ( α) ( is-orth-α)
           ( has-unique-extensions-is-local-type I ψ ϕ A is-local-A))
 ```
+
+Weak extension extensionality says that every contractible type
+has unique extensions for every shape inclusion `ϕ ⊂ ψ`.
+
+```rzk
+#def has-unique-extensions-is-contr uses (weakextext)
+  ( C : U)
+  ( is-contr-C : is-contr C)
+  : has-unique-extensions I ψ ϕ C
+  :=
+    weakextext I ψ ϕ
+    ( \ _ → C) ( \ _ → is-contr-C)
+
+#def has-unique-extensions-Unit uses (weakextext)
+  : has-unique-extensions I ψ ϕ Unit
+  := has-unique-extensions-is-contr Unit is-contr-Unit
+
+#end stability-properties-local-types
+```
+
+### Proof of second alternative characterization
+
+Next we prove the logical equivalence between `has-unique-extensions` and
+`is-right-orthogonal-to-shape-terminal-map`.
+This follows directly from the fact that `Unit` has unique extensions
+(using `weakextext : WeakExtExt`).
+
+```rzk
+#section is-right-orthogonal-to-shape-terminal-map
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+#variable A : U
+
+#def has-unique-extensions-is-right-orthogonal-to-shape-terminal-map
+  uses (weakextext)
+  ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-to-shape-terminal-map I ψ ϕ A)
+  : has-unique-extensions I ψ ϕ A
+  :=
+    has-unique-extensions-right-orthogonal-has-unique-extensions
+      I ψ ϕ A Unit (terminal-map A)
+    ( is-orth-ψ-ϕ-tm-A)
+    ( has-unique-extensions-Unit I ψ ϕ)
+
+#def is-right-orthogonal-to-shape-terminal-map-has-unique-extensions
+  uses (weakextext)
+  ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A)
+  : is-right-orthogonal-to-shape-terminal-map I ψ ϕ A
+  :=
+    is-right-orthogonal-have-unique-extensions I ψ ϕ A Unit
+    ( has-ue-ψ-ϕ-A) ( has-unique-extensions-Unit I ψ ϕ)
+    ( terminal-map A)
+
+#def is-right-orthogonal-to-shape-terminal-map-is-local-type
+  uses (weakextext)
+  ( is-lt-ψ-ϕ-A : is-local-type I ψ ϕ A)
+  : is-right-orthogonal-to-shape-terminal-map I ψ ϕ A
+  :=
+    is-right-orthogonal-to-shape-terminal-map-has-unique-extensions
+    ( has-unique-extensions-is-local-type I ψ ϕ A is-lt-ψ-ϕ-A)
+
+#def is-local-type-is-right-orthogonal-to-shape-terminal-map
+  uses (weakextext)
+  ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-to-shape-terminal-map I ψ ϕ A)
+  : is-local-type I ψ ϕ A
+  :=
+    is-local-type-has-unique-extensions I ψ ϕ A
+    ( has-unique-extensions-is-right-orthogonal-to-shape-terminal-map
+      ( is-orth-ψ-ϕ-tm-A))
+
+#end is-right-orthogonal-to-shape-terminal-map
+```
diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 3366ba3a..996bde40 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -415,7 +415,7 @@ type, then so is `A'`.
   : is-segal A'
   :=
     is-segal-is-local-horn-inclusion A'
-      ( is-local-type-domain-right-orthogonal-is-local-type-codomain
+      ( is-local-type-right-orthogonal-is-local-type
         ( 2 × 2) Δ² ( \ ts → Λ ts) A' A α
         ( is-inner-fibration-is-left-fibration A' A α is-left-fib-α)
         ( is-local-horn-inclusion-is-segal A is-segal-A))

From 4924c5ff5efcc8a2f3360befe58da886e6831071 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Wed, 11 Oct 2023 16:44:14 +0200
Subject: [PATCH 03/10] fiber products and relative products

---
 src/hott/11-homotopy-pullbacks.rzk.md | 111 ++++++++++++++++++++++++++
 1 file changed, 111 insertions(+)

diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index 972814f4..87cd0b27 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -411,3 +411,114 @@ from composition and cancelling laws for equivalences.
 
 #end homotopy-cartesian-horizontal-calculus
 ```
+
+## Fiber products
+
+Given two type families `B C : A → U`, we can form their fiberwise product.
+
+```rzk
+#def fiberwise-product
+  ( A : U)
+  ( B C : A → U)
+  : A → U
+  :=
+    \ a → product (B a) (C a)
+
+#def first-fiberwise-product
+  ( A : U)
+  ( B C : A → U)
+  ( a : A)
+  : fiberwise-product A B C a → B a
+  := \ (b,_) → b
+
+#def second-fiberwise-product
+  ( A : U)
+  ( B C : A → U)
+  ( a : A)
+  : fiberwise-product A B C a → C a
+  := \ (_,c) → c
+```
+
+Given two maps `B → A` and `C → A`, we can form the relative product over `A`.
+
+```rzk
+#section relative-product
+
+#variable A : U
+#variable B : U
+#variable β : B → A
+#variable C : U
+#variable γ : C → A
+
+#def relative-product
+  : U
+  := Σ ( (b, c) : product B C) , β b = γ c
+
+#def first-relative-product uses (A B β C γ)
+  : relative-product → B
+  := \ ((b , _), _) → b
+
+#def second-relative-product uses (A B β C γ)
+  : relative-product → C
+  := \ ((_ , c), _) → c
+```
+
+This relative product agrees with the fiber product obtained by summing
+over the product of all fibers.
+
+```rzk
+#def fiber-product
+  : U
+  := total-type A (fiberwise-product A (fib B A β) (fib C A γ))
+
+#def fiber-product-unpacked
+  : fiber-product
+  = ( Σ (a : A), (product (fib B A β a) (fib C A γ a)))
+  := refl
+
+#def relative-fiber-product uses (B C)
+  ( (a, ((b, p), (c,q))) : fiber-product )
+  : relative-product
+  := ( ( b , c) , zig-zag-concat A (β b) a (γ c) p q)
+
+#def fiber-relative-product uses ( A B β C)
+  ( ((b,c), e) : relative-product)
+  : fiber-product
+  := ( γ c , ( (b , e) , (c , refl)))
+
+#def is-id-relative-fiber-relative-product
+  ( bce : relative-product)
+  : relative-fiber-product (fiber-relative-product bce) = bce
+  := refl
+
+#def is-id-fiber-relative-fiber-product
+  : ( abpcq : fiber-product)
+  → ( fiber-relative-product (relative-fiber-product abpcq)) = abpcq
+  :=
+  \ (a', (bq', cq')) →
+    ind-fib C A γ
+    ( \ a cq →
+      ( ( bq : fib B A β a)
+      → ( fiber-relative-product (relative-fiber-product (a, (bq, cq)))
+        = ( a, (bq, cq)))))
+    ( \ c bq → refl)
+    ( a')
+    ( cq')
+    ( bq')
+
+#def is-equiv-relative-fiber-product uses (A B β C γ)
+  : is-equiv fiber-product relative-product relative-fiber-product
+  :=
+    ( ( fiber-relative-product
+      , is-id-fiber-relative-fiber-product)
+    , ( fiber-relative-product
+      , is-id-relative-fiber-relative-product))
+
+#def equiv-relative-product-fiber-product uses (A B β C γ)
+  : Equiv fiber-product relative-product
+  :=
+    ( relative-fiber-product
+    , is-equiv-relative-fiber-product)
+
+#end relative-product
+```

From 3f7bc117a4470deb9bab5091094c2ba46bd137ef Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Wed, 11 Oct 2023 16:54:57 +0200
Subject: [PATCH 04/10] fill region

---
 src/hott/11-homotopy-pullbacks.rzk.md | 25 ++++++++++++-------------
 1 file changed, 12 insertions(+), 13 deletions(-)

diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index 87cd0b27..e4a0eb2d 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -35,8 +35,8 @@ We start by fixing the data of a map between two type families
   := \ (a', c') → (α a', γ a' c')
 ```
 
-We say that such a square is homotopy cartesian
-just if it induces an equivalence componentwise.
+We say that such a square is homotopy cartesian just if it induces an
+equivalence componentwise.
 
 ```rzk
 #def is-homotopy-cartesian uses (A)
@@ -216,8 +216,8 @@ always do this (whether the square is homotopy-cartesian or not).
 
 ### Invariance under pullbacks
 
-We can pullback a homotopy cartesian square over `α : A' → A`
-along any map of maps `β → α` and obtain another homotopy cartesian square.
+We can pullback a homotopy cartesian square over `α : A' → A` along any map of
+maps `β → α` and obtain another homotopy cartesian square.
 
 ```rzk
 #def is-homotopy-cartesian-pullback
@@ -246,16 +246,15 @@ along any map of maps `β → α` and obtain another homotopy cartesian square.
 
 ## Pasting calculus for homotopy cartesian squares
 
-Currently our notion of squares is not symmetric,
-since the vertical maps are given by type families,
-i.e. they are _display maps_,
-while the horizontal maps are arbitrary.
-Therefore we distinquish between the vertical and the horizontal pasting calculus.
+Currently our notion of squares is not symmetric, since the vertical maps are
+given by type families, i.e. they are _display maps_, while the horizontal maps
+are arbitrary. Therefore we distinquish between the vertical and the horizontal
+pasting calculus.
 
 ### Vertical calculus
 
-The following vertical composition and cancellation laws follow easily from
-the corresponding statements about equivalences established above.
+The following vertical composition and cancellation laws follow easily from the
+corresponding statements about equivalences established above.
 
 ```rzk
 #section homotopy-cartesian-vertical-calculus
@@ -463,8 +462,8 @@ Given two maps `B → A` and `C → A`, we can form the relative product over `A
   := \ ((_ , c), _) → c
 ```
 
-This relative product agrees with the fiber product obtained by summing
-over the product of all fibers.
+This relative product agrees with the fiber product obtained by summing over the
+product of all fibers.
 
 ```rzk
 #def fiber-product

From dc3476b5ec25ac60c66f4acf1f9ec98f38c0ad46 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Wed, 11 Oct 2023 17:42:38 +0200
Subject: [PATCH 05/10] add projections and homotopy to fiber product

---
 src/hott/11-homotopy-pullbacks.rzk.md | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index 33edb1b1..6fdbd16c 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -461,6 +461,11 @@ Given two maps `B → A` and `C → A`, we can form the relative product over `A
 #def second-relative-product uses (A B β C γ)
   : relative-product → C
   := \ ((_ , c), _) → c
+
+#def homotopy-relative-product uses (A B C)
+  ( (bc, p) : relative-product )
+  : β (first-relative-product (bc,p)) = γ (second-relative-product (bc,p))
+  := p
 ```
 
 This relative product agrees with the fiber product obtained by summing over the
@@ -476,6 +481,21 @@ product of all fibers.
   = ( Σ (a : A), (product (fib B A β a) (fib C A γ a)))
   := refl
 
+#def first-fiber-product uses (A B β C γ)
+  : fiber-product → B
+  := \ (_, ((b, _), _ )) → b
+
+#def second-fiber-product uses (A B β C γ)
+  : fiber-product → C
+  := \ (_, (_, (c, _))) → c
+
+#def homotopy-fiber-product uses (A B C)
+  : ( abpcq : fiber-product )
+  → β (first-fiber-product abpcq) = γ (second-fiber-product abpcq)
+  :=
+    \ ( a, ((b, p), (c,q))) →
+      zig-zag-concat A (β b) a (γ c) p q
+
 #def relative-fiber-product uses (B C)
   ( (a, ((b, p), (c,q))) : fiber-product )
   : relative-product

From 68057f6d47ba4349cb414e4c408f112ae0d34e63 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Thu, 12 Oct 2023 11:08:51 +0200
Subject: [PATCH 06/10] autoformat

---
 .../04-right-orthogonal.rzk.md                | 24 +++++++++----------
 1 file changed, 11 insertions(+), 13 deletions(-)

diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index 2e8e78b0..d161a3da 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -345,9 +345,9 @@ We can ask that the terminal map `A → Unit` is right orthogonal to `ϕ ⊂ ψ`
 ### Proof of first alternative characterization
 
 The equivalence between `is-local-type` and `has-unique-extensions` follows
-straightforwardly from the fact that for every `σ : ϕ → A`
-we have an equivalence between the extension type `(t : ψ) → A [ϕ t ↦ σ t]`
-and the fiber of the restriction map `(ψ → A) → (ϕ → A)`.
+straightforwardly from the fact that for every `σ : ϕ → A` we have an
+equivalence between the extension type `(t : ψ) → A [ϕ t ↦ σ t]` and the fiber
+of the restriction map `(ψ → A) → (ϕ → A)`.
 
 ```rzk
 #def is-local-type-has-unique-extensions
@@ -379,7 +379,6 @@ and the fiber of the restriction map `(ψ → A) → (ϕ → A)`.
 #end has-unique-extensions
 ```
 
-
 ### Properties of local types / unique extension types
 
 We fix a shape inclusion `ϕ ⊂ ψ`.
@@ -391,8 +390,8 @@ We fix a shape inclusion `ϕ ⊂ ψ`.
 #variable ϕ : ψ → TOPE
 ```
 
-Every map between types with unique extensions / local types
-is right orthogonal.
+Every map between types with unique extensions / local types is right
+orthogonal.
 
 ```rzk
 #def is-right-orthogonal-have-unique-extensions
@@ -422,8 +421,8 @@ is right orthogonal.
     ( has-unique-extensions-is-local-type I ψ ϕ A is-lt-ψ-ϕ-A)
 ```
 
-Conversely, the property of having unique extension
-can be pulled back along any right orthogonal map.
+Conversely, the property of having unique extension can be pulled back along any
+right orthogonal map.
 
 ```rzk
 #def has-unique-extensions-right-orthogonal-has-unique-extensions
@@ -452,8 +451,8 @@ can be pulled back along any right orthogonal map.
           ( has-unique-extensions-is-local-type I ψ ϕ A is-local-A))
 ```
 
-Weak extension extensionality says that every contractible type
-has unique extensions for every shape inclusion `ϕ ⊂ ψ`.
+Weak extension extensionality says that every contractible type has unique
+extensions for every shape inclusion `ϕ ⊂ ψ`.
 
 ```rzk
 #def has-unique-extensions-is-contr uses (weakextext)
@@ -474,9 +473,8 @@ has unique extensions for every shape inclusion `ϕ ⊂ ψ`.
 ### Proof of second alternative characterization
 
 Next we prove the logical equivalence between `has-unique-extensions` and
-`is-right-orthogonal-to-shape-terminal-map`.
-This follows directly from the fact that `Unit` has unique extensions
-(using `weakextext : WeakExtExt`).
+`is-right-orthogonal-to-shape-terminal-map`. This follows directly from the fact
+that `Unit` has unique extensions (using `weakextext : WeakExtExt`).
 
 ```rzk
 #section is-right-orthogonal-to-shape-terminal-map

From d6d8974d896843f79b9763f2aee1931e7f61aaa0 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Thu, 12 Oct 2023 11:15:15 +0200
Subject: [PATCH 07/10] remove outdated helpers

---
 src/simplicial-hott/08-covariant.rzk.md | 63 -------------------------
 1 file changed, 63 deletions(-)

diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 3366ba3a..92f4f1fd 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -593,12 +593,6 @@ Finally, we deduce the theorem by some straightforward logical bookkeeping.
 
 ## Total type of a covariant family over a Segal type
 
-We prove that the total type of a covariant family over a Segal type is a Segal
-type. We split the proof into intermediate steps. Let `A` be a type and a type
-family `#!rzk C : A → U`.
-
-### Category theoretic proof
-
 For every covariant family `C : A → U`, the projection `Σ A, C → A` is an left
 fibration, hence an inner fibration. It immediately follows that if `A` is
 Segal, then so is `Σ A, C`.
@@ -617,63 +611,6 @@ Segal, then so is `Σ A, C`.
             ( is-naive-left-fibration-is-covariant A C is-covariant-C))
 ```
 
-### Type theoretic proof
-
-We examine the fibers of the horn restriction on the total type of `C`. First
-note we have the equivalences:
-
-```rzk
-#def apply-4-3
-  ( A : U )
-  ( C : A → U )
-  : Equiv
-    ( Λ → (Σ ( a : A ), C a ) )
-    ( Σ ( f : Λ → A ), ( t : Λ ) → ( C ( f t ) ) )
-  :=
-    axiom-choice ( 2 × 2 ) Λ ( \ t → BOT ) ( \ t → A )
-    ( \ t a → C a ) ( \ t → recBOT ) ( \ t → recBOT )
-
-#def apply-4-3-again
-  ( A : U )
-  ( C : A → U )
-  : Equiv
-    ( Δ² → (Σ ( a : A ), C a ) )
-    ( Σ ( f : Δ² → A ), ( t : Δ² ) → ( C ( f t ) ) )
-  :=
-    axiom-choice ( 2 × 2 ) Δ² ( \ t → BOT ) ( \ t → A )
-    ( \ t a → C a ) ( \ t → recBOT ) ( \ t → recBOT )
-```
-
-We show that the induced map between this types is an equivalence. First we
-exhibit the map:
-
-```rzk
-#def total-inner-horn-restriction
-  ( A : U )
-  ( C : A → U )
-  : ( Σ ( f : Δ² → A ), ( t : Δ² ) → ( C ( f t ) ) ) →
-    ( Σ ( g : Λ → A ), ( t : Λ ) → ( C ( g t ) ) )
-  := \ ( f, μ ) → ( \ t → f t , \ t → μ t)
-```
-
-Next we compute the fibers of this map by showing the equivalence as claimed in
-the proof of Theorem 8.8 in RS17. The following maps will be packed into some
-`#!rzk Equiv`.
-
-```rzk
-#def map-to-total-inner-horn-restriction-fiber
-  ( A : U )
-  ( C : A → U )
-  ( (g , φ) : ( Σ ( k : Λ → A ), ( t : Λ ) → C ( k t ) ) )
-  : ( Σ (h : (t : Δ²) → A [ Λ t ↦ g t ] ) ,
-      (( t : Δ² ) → C (h t) [ Λ t ↦ φ t])) →
-    ( fib ( Σ ( l : Δ² → A ), ( t : Δ² ) → ( C ( l t ) ))
-          ( Σ ( k : Λ → A ), ( t : Λ ) → ( C ( k t ) ))
-          ( total-inner-horn-restriction A C )
-          ( g,  φ) )
-  := \ ( f,μ ) → ( ( \ t → f t, \ t → μ t  ), refl )
-```
-
 ## Representable covariant families
 
 If `A` is a Segal type and `a : A` is any term, then `hom A a` defines a

From 7261a929d2f3625b830d9da44a997ba289d2e692 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Thu, 12 Oct 2023 18:25:21 +0200
Subject: [PATCH 08/10] compute fiber product with unit type

---
 src/hott/11-homotopy-pullbacks.rzk.md | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index 6fdbd16c..a5514a80 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -542,3 +542,29 @@ product of all fibers.
 
 #end relative-product
 ```
+
+### Fiber product with singleton type
+
+The relative product of `β : B → A` with a map `Unit → A` corresponding to
+`a : A` is nothing but the fiber `fib B A β a`.
+
+```rzk
+#def compute-relative-product-singleton
+  ( A B : U)
+  ( β : B → A)
+  ( a : A)
+  : Equiv-of-maps
+    ( fib B A β a) (Unit) (\ _ → unit)
+    ( relative-product A B β Unit (\ unit → a))
+    ( Unit) ( second-relative-product A B β Unit (\ unit → a))
+  :=
+    ( ( ( ( \ (b , p) → ((b , unit) , p))
+        , ( identity Unit))
+      , \ _ → refl)
+    , ( ( ( ( \ ((b , unit) , p) → (b, p))
+          , ( \ _ → refl))
+        , ( ( \ ((b , unit) , p) → (b, p))
+          , ( \ _ → refl)))
+      , is-equiv-identity Unit))
+
+```

From ebc3aa67699063556f0e04649d8a8924f1a6dced Mon Sep 17 00:00:00 2001
From: Tashi Walde <tashi.walde@gmail.com>
Date: Fri, 13 Oct 2023 17:04:29 +0200
Subject: [PATCH 09/10] Apply suggestions from code review

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/hott/11-homotopy-pullbacks.rzk.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index a5514a80..bbe6209c 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -414,7 +414,7 @@ from composition and cancelling laws for equivalences.
 
 ## Fiber products
 
-Given two type families `B C : A → U`, we can form their fiberwise product.
+Given two type families `B C : A → U`, we can form their **fiberwise product**.
 
 ```rzk
 #def fiberwise-product
@@ -439,7 +439,7 @@ Given two type families `B C : A → U`, we can form their fiberwise product.
   := \ (_,c) → c
 ```
 
-Given two maps `B → A` and `C → A`, we can form the relative product over `A`.
+Given two maps `B → A` and `C → A`, we can form the **relative product** over `A`.
 
 ```rzk
 #section relative-product
@@ -452,7 +452,7 @@ Given two maps `B → A` and `C → A`, we can form the relative product over `A
 
 #def relative-product
   : U
-  := Σ ( (b, c) : product B C) , β b = γ c
+  := Σ ( (b, c) : product B C) , (β b = γ c)
 
 #def first-relative-product uses (A B β C γ)
   : relative-product → B
@@ -476,7 +476,7 @@ product of all fibers.
   : U
   := total-type A (fiberwise-product A (fib B A β) (fib C A γ))
 
-#def fiber-product-unpacked
+#def unpack-fiber-product
   : fiber-product
   = ( Σ (a : A), (product (fib B A β a) (fib C A γ a)))
   := refl

From e2149822477ee4bb0e901831b7de044e82a856f0 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@w199-8-v4.eduroam.dynamic.rbg.tum.de>
Date: Fri, 13 Oct 2023 17:07:44 +0200
Subject: [PATCH 10/10] autoformat

---
 src/hott/11-homotopy-pullbacks.rzk.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index bbe6209c..45aeb770 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -439,7 +439,8 @@ Given two type families `B C : A → U`, we can form their **fiberwise product**
   := \ (_,c) → c
 ```
 
-Given two maps `B → A` and `C → A`, we can form the **relative product** over `A`.
+Given two maps `B → A` and `C → A`, we can form the **relative product** over
+`A`.
 
 ```rzk
 #section relative-product