From d9a8fdd9638fc9b94792e5fd20130be47ca05b60 Mon Sep 17 00:00:00 2001
From: Jonathan Campbell <jonathan@pop-os.localdomain>
Date: Thu, 21 Sep 2023 17:34:08 +0200
Subject: [PATCH 01/15] added unchecked stuff

---
 src/simplicial-hott/04-extension-types.rzk.md | 47 +++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index a8c1dfd7..37ea06ed 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -297,6 +297,19 @@ Weak extension extensionality implies extension extensionality; this is the cont
             is-contr-based-paths (A t ) ((ext-projection-temp) t))
       ( \ t → (a t , refl) ) 
 
+#define is-contr-ext-codomain-based-paths uses (weak-ext-ext f) 
+    : is-contr 
+        ((t : ψ ) → (Σ (y : A t) ,
+                    (y = (ext-projection-temp) t))[ϕ t ↦ (a t , refl)])
+    := weak-ext-ext 
+        ( I )
+        ( ψ )
+        ( ϕ )
+        ( \t → (Σ (y : A t) , (y = (ext-projection-temp) t)))
+        (\ t → 
+            is-contr-codomain-based-paths (A t ) ((ext-projection-temp) t))
+        (\ t → (a t , refl) )  
+
 #define is-contr-based-paths-ext uses (weak-ext-ext)
   : is-contr (Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) , 
               (t : ψ ) → (f t = g t) [ϕ t ↦ refl])
@@ -450,3 +463,37 @@ equivalences of extension types. For simplicity, we extend from `#!rzk BOT`.
               ( b)
               ( \ t → second (second (second (famequiv t))) (b t))))))
 ```
+We have a homotopy extension property
+
+```rzk
+#define htpy-ext-property
+    ( weak-ext-ext : WeakExtExt)
+    ( I : CUBE)
+    ( ψ : I → TOPE)
+    ( ϕ : ψ → TOPE)
+    ( A : ψ → U)
+    ( b : (t : ψ ) → A t)
+    ( a : (t : ϕ ) → A t) 
+    ( e : (t : ϕ ) → a t = b t) 
+    : Σ (a' : (t : ψ ) → A t [ϕ t ↦ a t]) , 
+        ((t : ψ ) → (a' t = b t) [ϕ t ↦ e t])
+    := 
+      first (
+       axiom-choice
+        ( I )
+        ( ψ ) 
+        ( ϕ ) 
+        ( A ) 
+        ( \ t y → y = (ext-projection-temp) t)
+        ( a ) 
+        ( e ))  (first ( weak-ext-ext 
+          ( I )
+          ( ψ )
+          ( ϕ )
+          ( \t → (Σ (y : A t) , (y = (ext-projection-temp) t)))
+          (\ t → is-contr-codomain-based-paths 
+                  (A t )
+                  ((ext-projection-temp) t))
+          (\ t → (a t , e t) )))
+
+```
\ No newline at end of file

From 68104a07dc44f06762ab700965c9950e1fe9301e Mon Sep 17 00:00:00 2001
From: Kenji Maillard <kenji@maillard.blue>
Date: Thu, 21 Sep 2023 18:01:20 +0200
Subject: [PATCH 02/15]  Proof of the naturality equation (Prop 6.6)

---
 .../06-2cat-of-segal-types.rzk.md             | 53 +++++++++++++++++++
 1 file changed, 53 insertions(+)

diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
index ea2ab5b1..b83b38a4 100644
--- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
+++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
@@ -318,3 +318,56 @@ the "Gray interchanger" built from two commutative triangles.
     ( horizontal-comp-nat-trans A B C f g f' g' η η')
   := \ (t, s) a → η' t (η s a)
 ```
+
+### Naturality square
+
+```rzk title="RS17, Proposition 6.6"
+#section eq-from-square
+
+#variable A : U
+#variable is-segal-A : is-segal A
+#variable α : (Δ¹×Δ¹) → A
+
+#def α00 : A := α (0₂,0₂)
+#def α01 : A := α (0₂,1₂)
+#def α10 : A := α (1₂,0₂)
+#def α11 : A := α (1₂,1₂)
+
+#def α0* : Δ¹ → A := \ t → α (0₂,t)
+#def α1* : Δ¹ → A := \ t → α (1₂,t)
+#def α*0 : Δ¹ → A := \ s → α (s,0₂)
+#def α*1 : Δ¹ → A := \ s → α (s,1₂)
+#def α-diag : Δ¹ → A := \ s → α (s,s)
+
+#def lhs uses (α) : Δ¹ → A := comp-is-segal A is-segal-A α00 α01 α11 α0* α*1
+#def rhs uses (α) : Δ¹ → A := comp-is-segal A is-segal-A α00 α10 α11 α*0 α1*
+
+#def lower-triangle : hom2 A α00 α01 α11 α0* α*1 α-diag
+  := \ (s, t) → α (t,s)
+
+#def upper-triangle : hom2 A α00 α10 α11 α*0 α1* α-diag
+  := \ (s,t) → α (s,t)
+
+#def eq-from-square uses (α)
+  : comp-is-segal A is-segal-A α00 α01 α11 α0* α*1
+    = comp-is-segal A is-segal-A α00 α10 α11 α*0 α1*
+  :=
+    zig-zag-concat (hom A α00 α11) lhs α-diag rhs
+      (uniqueness-comp-is-segal A is-segal-A α00 α01 α11 α0* α*1 α-diag lower-triangle)
+      (uniqueness-comp-is-segal A is-segal-A α00 α10 α11 α*0 α1* α-diag upper-triangle)
+
+
+#end eq-from-square
+
+#def naturality-eq
+  (A B : U)
+  (is-segal-B : is-segal B)
+  (f g : A → B)
+  (α : hom (A → B) f g)
+  (x y : A)
+  (k : hom A x y)
+  : comp-is-segal B is-segal-B (f x) (f y) (g y) (ap-hom A B f x y k) (\ s → α s y)
+    = comp-is-segal B is-segal-B (f x) (g x) (g y) (\ s → α s x) (ap-hom A B g x y k)
+  := eq-from-square B is-segal-B (\ (s,t) → α s (k t))
+
+```

From c0826f8d233b343603cbe88e81823cd46e0340bd Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Fri, 22 Sep 2023 11:40:51 +0200
Subject: [PATCH 03/15] right cancellation of equivalences, pasting of
 pullbacks

---
 src/hott/03-equivalences.rzk.md     | 37 +++++++++++++++++++
 src/hott/08-families-of-maps.rzk.md | 57 +++++++++++++++++++++++++++++
 2 files changed, 94 insertions(+)

diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md
index b64d7c74..359ab579 100644
--- a/src/hott/03-equivalences.rzk.md
+++ b/src/hott/03-equivalences.rzk.md
@@ -314,6 +314,43 @@ Now we compose the functions that are equivalences.
   := equiv-comp B A C (inv-equiv A B A≃B) (A≃C)
 ```
 
+```rzk title="Right cancellation of equivalence property in diagrammatic order"
+#def ap-cancel-has-retraction
+  ( B C : U)
+  ( g : B → C)
+  ( (retr-g, η-g) : has-retraction B C g)
+  ( b b' : B)
+  : (g b = g b') → (b = b')
+  :=
+    \ gp →
+      triple-concat B b (retr-g (g b)) (retr-g (g b')) b'
+        (rev B (retr-g (g b)) b
+          (η-g b))
+        (ap C B (g b) (g b') retr-g gp)
+        (η-g b')
+
+
+#def is-equiv-right-cancel
+  ( A B C : U)
+  ( f : A → B)
+  ( g : B → C)
+  ( (has-retraction-g, (sec-g, ε-g)) : is-equiv B C g)
+  ( ((retr-gf, η-gf), (sec-gf, ε-gf)) : is-equiv A C (comp A B C g f))
+  : is-equiv A B f
+  :=
+    ( (comp B C A
+      retr-gf g,
+    η-gf) ,
+    (comp B C A
+      sec-gf g,
+    \ b → -- need (f ∘ sec-gf ∘ g) b = b
+      ap-cancel-has-retraction B C g has-retraction-g (f (sec-gf (g b))) b
+      (ε-gf (g b)) -- have g (f ∘ sec-gf ∘ g) b) = g b
+    )
+    )
+
+```
+
 ```rzk title="A composition of three equivalences"
 #def equiv-triple-comp
   ( A B C D : U)
diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md
index e94084e5..695d2e08 100644
--- a/src/hott/08-families-of-maps.rzk.md
+++ b/src/hott/08-families-of-maps.rzk.md
@@ -812,3 +812,60 @@ types over a product type.
 
 #end fibered-map-over-product
 ```
+
+## Homotopy cartesian squares
+
+
+```rzk
+#def is-homotopy-cartesian
+  ( A' : U)
+  ( C' : A' → U)
+  ( A : U)
+  ( C : A → U)
+  ( f : A' → A)
+  ( F : (a' : A') → C' a' → C (f a'))
+  : U
+  :=
+    (a' : A') → is-equiv (C' a') (C (f a')) (F a')
+
+#def homotopy-cartesian-square
+  ( A' : U)
+  ( C' : A' → U)
+  ( A : U)
+  ( C : A → U)
+  : U
+  := Σ (f : A' → A), Σ (F : (a' : A') → C' a' → C (f a')),
+    is-homotopy-cartesian A' C' A C f F
+
+
+#section homotopy-cartesian-pasting
+
+#variable A'' : U
+#variable C'' : A'' → U
+#variable A' : U
+#variable C' : A' → U
+#variable A : U
+#variable C : A → U
+#variable f' : A'' → A'
+#variable F' : (a'' : A'') → C'' a'' → C' (f' a'')
+#variable f : A' → A
+#variable F : (a' : A') → C' a' → C (f a')
+
+#def is-homotopy-cartesian-composition
+  : is-homotopy-cartesian A'' C'' A' C' f' F' →
+    is-homotopy-cartesian A' C' A C f F →
+    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'')
+      )
+  :=
+    \ ihc' ihc a'' →
+    is-equiv-comp (C'' a'') (C' (f' a'')) (C (f (f' a'')))
+      (F' a'') (ihc' a'')
+      (F (f' a'')) (ihc (f' a''))
+
+#end homotopy-cartesian-pasting
+```

From a87c1d5635f2a81949c88884c4813e0bca8947e9 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Fri, 22 Sep 2023 11:54:47 +0200
Subject: [PATCH 04/15] right cancellation of homotopy cartesian squares

---
 src/hott/08-families-of-maps.rzk.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md
index 695d2e08..8f82cb80 100644
--- a/src/hott/08-families-of-maps.rzk.md
+++ b/src/hott/08-families-of-maps.rzk.md
@@ -867,5 +867,21 @@ types over a product type.
       (F' a'') (ihc' a'')
       (F (f' a'')) (ihc (f' a''))
 
+#def is-homotopy-cartesian-cancellation
+  : is-homotopy-cartesian A' C' A C f F
+  → 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'
+  :=
+    \ ihc ihc'' a'' →
+    is-equiv-right-cancel (C'' a'') (C' (f' a'')) (C (f (f' a'')))
+      (F' a'') (F (f' a''))
+      (ihc (f' a''))
+      (ihc'' a'')
+
 #end homotopy-cartesian-pasting
 ```

From d1a17b744adb44aa71514028558e45555d1e573d Mon Sep 17 00:00:00 2001
From: Jonathan Campbell <jonathan@pop-os.localdomain>
Date: Fri, 22 Sep 2023 12:18:13 +0200
Subject: [PATCH 05/15] added the homotopy extension property, prop 4.10

---
 src/simplicial-hott/04-extension-types.rzk.md | 80 ++++++++++++-------
 1 file changed, 51 insertions(+), 29 deletions(-)

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 3223a6a5..d512fd4b 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -268,7 +268,7 @@ We refer to another form as an "extension extensionality" axiom.
 Weak extension extensionality implies extension extensionality; this is the
 context of RS17 Proposition 4.8 (i). We prove this in a series of lemmas. The
 `ext-projection-temp` function is a (hopefully temporary) helper that explicitly
-cases an extension type to a function type.
+cases an extension type to a function type. 
 
 ```rzk
 #section rs-4-8
@@ -478,37 +478,59 @@ equivalences of extension types. For simplicity, we extend from `#!rzk BOT`.
               ( b)
               ( \ t → second (second (second (famequiv t))) (b t))))))
 ```
-We have a homotopy extension property
+We have a homotopy extension property. 
+
+The following code is another instantiation of casting, necessary for some arguments below. 
 
 ```rzk
-#define htpy-ext-property
-    ( weak-ext-ext : WeakExtExt)
+#define restrict
     ( I : CUBE)
     ( ψ : I → TOPE)
     ( ϕ : ψ → TOPE)
-    ( A : ψ → U)
-    ( b : (t : ψ ) → A t)
-    ( a : (t : ϕ ) → A t) 
-    ( e : (t : ϕ ) → a t = b t) 
-    : Σ (a' : (t : ψ ) → A t [ϕ t ↦ a t]) , 
-        ((t : ψ ) → (a' t = b t) [ϕ t ↦ e t])
-    := 
-      first (
-       axiom-choice
+    ( A : ψ → U) 
+    ( a : (t : ϕ) → A t) 
+    ( f : (t : ψ) → A t [ϕ t ↦ a t]) 
+    : (t : ψ ) → A t
+    := f
+
+```
+
+The homotopy extension property follows from a straightforward application of the axiom of choice
+to the point of contraction for weak extension extensionality. 
+
+```rzk title="RS17 Proposition 4.10"
+#define htpy-ext-property
+  ( weak-ext-ext : WeakExtExt)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A : ψ → U)
+  ( b : (t : ψ ) → A t)
+  ( a : (t : ϕ ) → A t) 
+  ( e : (t : ϕ ) → a t = b t) 
+  : Σ (a' : (t : ψ ) → A t [ϕ t ↦ a t]) , 
+      ((t : ψ ) → (restrict I ψ ϕ A a a' t = b t) [ϕ t ↦ e t])
+  := 
+    first 
+    ( axiom-choice --- apply the forward equivalence of AoC
+      ( I )
+      ( ψ ) 
+      ( ϕ ) 
+      ( A ) 
+      ( \ t y → y = b t)
+      ( a ) 
+      ( e ))  
+    ( first --- to the center of a contractible extension type
+             --- obtained from weak-ext-ext
+      ( weak-ext-ext 
         ( I )
-        ( ψ ) 
-        ( ϕ ) 
-        ( A ) 
-        ( \ t y → y = (ext-projection-temp) t)
-        ( a ) 
-        ( e ))  (first ( weak-ext-ext 
-          ( I )
-          ( ψ )
-          ( ϕ )
-          ( \t → (Σ (y : A t) , (y = (ext-projection-temp) t)))
-          (\ t → is-contr-codomain-based-paths 
-                  (A t )
-                  ((ext-projection-temp) t))
-          (\ t → (a t , e t) )))
-
-```
\ No newline at end of file
+        ( ψ )
+        ( ϕ )
+        ( \t → (Σ (y : A t) , (y = b t)))
+        ( \ t → is-contr-codomain-based-paths 
+                ( A t )
+                ( (b t)))
+        ( \ t → ( a t , e t) )))
+
+```
+

From 77ef6223c69d552fa6bc2388e6eec43278b21a48 Mon Sep 17 00:00:00 2001
From: Kenji Maillard <kenji@maillard.blue>
Date: Fri, 22 Sep 2023 13:04:40 +0200
Subject: [PATCH 06/15] naming and formatting changes

---
 .../06-2cat-of-segal-types.rzk.md             | 33 +++++++++++--------
 1 file changed, 19 insertions(+), 14 deletions(-)

diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
index b83b38a4..8e308883 100644
--- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
+++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
@@ -322,7 +322,7 @@ the "Gray interchanger" built from two commutative triangles.
 ### Naturality square
 
 ```rzk title="RS17, Proposition 6.6"
-#section eq-from-square
+#section comp-eq-square-is-segal
 
 #variable A : U
 #variable is-segal-A : is-segal A
@@ -342,32 +342,37 @@ the "Gray interchanger" built from two commutative triangles.
 #def lhs uses (α) : Δ¹ → A := comp-is-segal A is-segal-A α00 α01 α11 α0* α*1
 #def rhs uses (α) : Δ¹ → A := comp-is-segal A is-segal-A α00 α10 α11 α*0 α1*
 
-#def lower-triangle : hom2 A α00 α01 α11 α0* α*1 α-diag
+#def lower-triangle-square : hom2 A α00 α01 α11 α0* α*1 α-diag
   := \ (s, t) → α (t,s)
 
-#def upper-triangle : hom2 A α00 α10 α11 α*0 α1* α-diag
+#def upper-triangle-square : hom2 A α00 α10 α11 α*0 α1* α-diag
   := \ (s,t) → α (s,t)
 
-#def eq-from-square uses (α)
-  : comp-is-segal A is-segal-A α00 α01 α11 α0* α*1
-    = comp-is-segal A is-segal-A α00 α10 α11 α*0 α1*
+#def comp-eq-square-is-segal uses (α)
+  : comp-is-segal A is-segal-A α00 α01 α11 α0* α*1 =
+    comp-is-segal A is-segal-A α00 α10 α11 α*0 α1*
   :=
     zig-zag-concat (hom A α00 α11) lhs α-diag rhs
-      (uniqueness-comp-is-segal A is-segal-A α00 α01 α11 α0* α*1 α-diag lower-triangle)
-      (uniqueness-comp-is-segal A is-segal-A α00 α10 α11 α*0 α1* α-diag upper-triangle)
+    ( uniqueness-comp-is-segal A is-segal-A α00 α01 α11 α0* α*1 α-diag
+      ( lower-triangle-square))
+    ( uniqueness-comp-is-segal A is-segal-A α00 α10 α11 α*0 α1* α-diag
+      ( upper-triangle-square))
 
 
-#end eq-from-square
+#end comp-eq-square-is-segal
 
-#def naturality-eq
+#def naturality-nat-trans-is-segal
   (A B : U)
   (is-segal-B : is-segal B)
   (f g : A → B)
   (α : hom (A → B) f g)
   (x y : A)
   (k : hom A x y)
-  : comp-is-segal B is-segal-B (f x) (f y) (g y) (ap-hom A B f x y k) (\ s → α s y)
-    = comp-is-segal B is-segal-B (f x) (g x) (g y) (\ s → α s x) (ap-hom A B g x y k)
-  := eq-from-square B is-segal-B (\ (s,t) → α s (k t))
-
+  : comp-is-segal B is-segal-B (f x) (f y) (g y)
+    ( ap-hom A B f x y k)
+    ( \ s → α s y) =
+    comp-is-segal B is-segal-B (f x) (g x) (g y)
+    ( \ s → α s x)
+    ( ap-hom A B g x y k)
+  := comp-eq-square-is-segal B is-segal-B (\ (s,t) → α s (k t))
 ```

From 7af1390f964f9b0766325165a67895cb7a2b40f0 Mon Sep 17 00:00:00 2001
From: Jonathan Campbell <jonathan@pop-os.localdomain>
Date: Fri, 22 Sep 2023 13:53:19 +0200
Subject: [PATCH 07/15] removed comments

---
 src/simplicial-hott/04-extension-types.rzk.md | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index d512fd4b..2b57bcc0 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -512,7 +512,7 @@ to the point of contraction for weak extension extensionality.
       ((t : ψ ) → (restrict I ψ ϕ A a a' t = b t) [ϕ t ↦ e t])
   := 
     first 
-    ( axiom-choice --- apply the forward equivalence of AoC
+    ( axiom-choice 
       ( I )
       ( ψ ) 
       ( ϕ ) 
@@ -520,8 +520,7 @@ to the point of contraction for weak extension extensionality.
       ( \ t y → y = b t)
       ( a ) 
       ( e ))  
-    ( first --- to the center of a contractible extension type
-             --- obtained from weak-ext-ext
+    ( first 
       ( weak-ext-ext 
         ( I )
         ( ψ )

From 6f8b771f3f17901c0cf4eccd63342e99297d5e75 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Fri, 22 Sep 2023 13:28:42 +0200
Subject: [PATCH 08/15] slices and coslices are functorial

---
 src/simplicial-hott/05-segal-types.rzk.md | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index 2ccccfb6..62d26f99 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -72,6 +72,25 @@ are called the coslice and slice, respectively.
   := Σ (z : A) , (hom A z a)
 ```
 
+The types `coslice A a` and `slice A a`
+are functorial in `A` in the following sense:
+
+```rzk"
+#def coslice-fun
+  (A B : U)
+  (f : A → B)
+  : (a : A) → coslice A a → coslice B (f a)
+  :=
+    \ (a', g) → (f a', \ t → f (g t))
+
+#def slice-fun
+  (A B : U)
+  (f : A → B)
+  : (a : A) → slice A a → slice B (f a)
+  :=
+    \ (a', g) → (f a', \ t → f (g t))
+```
+
 Extension types are also used to define the type of commutative triangles:
 
 <svg style="float: right" viewBox="0 0 200 200" width="150" height="200">

From 8d2963945ab065a084c0fe35f7b316e7644de923 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Fri, 22 Sep 2023 14:14:11 +0200
Subject: [PATCH 09/15] typo

---
 src/simplicial-hott/05-segal-types.rzk.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index 62d26f99..7a4fbfe0 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -75,7 +75,7 @@ are called the coslice and slice, respectively.
 The types `coslice A a` and `slice A a`
 are functorial in `A` in the following sense:
 
-```rzk"
+```rzk
 #def coslice-fun
   (A B : U)
   (f : A → B)

From 2f4e5fb72067ca06ce15a43788cd68441fbbf94c Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Fri, 22 Sep 2023 14:19:41 +0200
Subject: [PATCH 10/15] typo

---
 src/simplicial-hott/05-segal-types.rzk.md | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index 7a4fbfe0..22c240bb 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -79,14 +79,16 @@ are functorial in `A` in the following sense:
 #def coslice-fun
   (A B : U)
   (f : A → B)
-  : (a : A) → coslice A a → coslice B (f a)
+  (a : A)
+  : coslice A a → coslice B (f a)
   :=
     \ (a', g) → (f a', \ t → f (g t))
 
 #def slice-fun
   (A B : U)
   (f : A → B)
-  : (a : A) → slice A a → slice B (f a)
+  (a : A)
+  : slice A a → slice B (f a)
   :=
     \ (a', g) → (f a', \ t → f (g t))
 ```

From 80a87e2348dc93e83ba5dbef5c25b7f72afa10e4 Mon Sep 17 00:00:00 2001
From: jonalfcam <jonalfcam@gmail.com>
Date: Sat, 23 Sep 2023 13:24:52 +0200
Subject: [PATCH 11/15] Update src/simplicial-hott/04-extension-types.rzk.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/simplicial-hott/04-extension-types.rzk.md | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 2b57bcc0..cfc8530d 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -299,8 +299,9 @@ cases an extension type to a function type.
 
 #define is-contr-ext-codomain-based-paths uses (weak-ext-ext f) 
     : is-contr 
-        ((t : ψ ) → (Σ (y : A t) ,
-                    (y = (ext-projection-temp) t))[ϕ t ↦ (a t , refl)])
+        ( ( t : ψ) →
+          ( Σ (y : A t) , (y = ext-projection-temp t))
+          [ ϕ t ↦ (a t , refl)])
     := weak-ext-ext 
         ( I )
         ( ψ )

From d9e91e76338f53f1ee114c3bfeef8a1c4386a348 Mon Sep 17 00:00:00 2001
From: jonalfcam <jonalfcam@gmail.com>
Date: Sat, 23 Sep 2023 13:25:09 +0200
Subject: [PATCH 12/15] Update src/simplicial-hott/04-extension-types.rzk.md

Co-authored-by: Nikolai Kudasov <fizruk@users.noreply.github.com>
---
 src/simplicial-hott/04-extension-types.rzk.md | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index cfc8530d..0e74981a 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -303,13 +303,12 @@ cases an extension type to a function type.
           ( Σ (y : A t) , (y = ext-projection-temp t))
           [ ϕ t ↦ (a t , refl)])
     := weak-ext-ext 
-        ( I )
-        ( ψ )
-        ( ϕ )
-        ( \t → (Σ (y : A t) , (y = (ext-projection-temp) t)))
-        (\ t → 
-            is-contr-codomain-based-paths (A t ) ((ext-projection-temp) t))
-        (\ t → (a t , refl) )  
+        ( I)
+        ( ψ)
+        ( ϕ)
+        ( \ t → (Σ (y : A t) , y = ext-projection-temp t))
+        ( \ t → is-contr-codomain-based-paths (A t) (ext-projection-temp t))
+        ( \ t → (a t , refl))
 
 #define is-contr-based-paths-ext uses (weak-ext-ext)
   : is-contr (Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,

From f38feb73b40e72bb0eed4ddca4d1cd40b5c37f26 Mon Sep 17 00:00:00 2001
From: jonalfcam <jonalfcam@gmail.com>
Date: Sat, 23 Sep 2023 13:25:24 +0200
Subject: [PATCH 13/15] Update src/simplicial-hott/04-extension-types.rzk.md

Co-authored-by: Nikolai Kudasov <fizruk@users.noreply.github.com>
---
 src/simplicial-hott/04-extension-types.rzk.md | 35 +++++++++----------
 1 file changed, 17 insertions(+), 18 deletions(-)

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 0e74981a..ec4d818a 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -505,31 +505,30 @@ to the point of contraction for weak extension extensionality.
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
   ( A : ψ → U)
-  ( b : (t : ψ ) → A t)
-  ( a : (t : ϕ ) → A t) 
-  ( e : (t : ϕ ) → a t = b t) 
-  : Σ (a' : (t : ψ ) → A t [ϕ t ↦ a t]) , 
-      ((t : ψ ) → (restrict I ψ ϕ A a a' t = b t) [ϕ t ↦ e t])
+  ( b : (t : ψ) → A t)
+  ( a : (t : ϕ) → A t) 
+  ( e : (t : ϕ) → a t = b t) 
+  : Σ (a' : (t : ψ) → A t [ϕ t ↦ a t]) , 
+      ((t : ψ) → (restrict I ψ ϕ A a a' t = b t) [ϕ t ↦ e t])
   := 
     first 
     ( axiom-choice 
-      ( I )
-      ( ψ ) 
-      ( ϕ ) 
-      ( A ) 
+      ( I)
+      ( ψ) 
+      ( ϕ) 
+      ( A) 
       ( \ t y → y = b t)
-      ( a ) 
-      ( e ))  
+      ( a) 
+      ( e))  
     ( first 
       ( weak-ext-ext 
-        ( I )
-        ( ψ )
-        ( ϕ )
-        ( \t → (Σ (y : A t) , (y = b t)))
+        ( I)
+        ( ψ)
+        ( ϕ)
+        ( \ t → (Σ (y : A t) , y = b t))
         ( \ t → is-contr-codomain-based-paths 
-                ( A t )
-                ( (b t)))
+                ( A t)
+                ( b t))
         ( \ t → ( a t , e t) )))
-
 ```
 

From 7a93e8f807e6d57e861d14490151dec380e32c9f Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Sat, 23 Sep 2023 18:15:30 +0200
Subject: [PATCH 14/15] Add rzk.yaml to specify project files

---
 rzk.yaml | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 rzk.yaml

diff --git a/rzk.yaml b/rzk.yaml
new file mode 100644
index 00000000..4c2fc69f
--- /dev/null
+++ b/rzk.yaml
@@ -0,0 +1,3 @@
+include:
+  - src/hott/**/*.rzk.md
+  - src/simplicial-hott/**/*.rzk.md

From 1a14276f902f6232dc27a40d8eba206c4c58c0a6 Mon Sep 17 00:00:00 2001
From: emilyriehl <emilyriehl@math.jhu.edu>
Date: Sat, 23 Sep 2023 21:01:05 +0200
Subject: [PATCH 15/15] deleted unnecessary indentation

---
 src/simplicial-hott/04-extension-types.rzk.md | 125 +++++++++---------
 1 file changed, 64 insertions(+), 61 deletions(-)

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index ec4d818a..3656eed7 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -268,7 +268,7 @@ We refer to another form as an "extension extensionality" axiom.
 Weak extension extensionality implies extension extensionality; this is the
 context of RS17 Proposition 4.8 (i). We prove this in a series of lemmas. The
 `ext-projection-temp` function is a (hopefully temporary) helper that explicitly
-cases an extension type to a function type. 
+cases an extension type to a function type.
 
 ```rzk
 #section rs-4-8
@@ -288,27 +288,28 @@ cases an extension type to a function type.
 #define is-contr-ext-based-paths uses (weak-ext-ext f)
   : is-contr ((t : ψ ) → (Σ (y : A t) ,
               ((ext-projection-temp) t = y))[ϕ t ↦ (a t , refl)])
-  := weak-ext-ext
-      ( I )
-      ( ψ )
-      ( ϕ )
-      ( \ t → (Σ (y : A t) , ((ext-projection-temp) t = y)))
-      ( \ t →
-            is-contr-based-paths (A t ) ((ext-projection-temp) t))
-      ( \ t → (a t , refl) )
-
-#define is-contr-ext-codomain-based-paths uses (weak-ext-ext f) 
-    : is-contr 
-        ( ( t : ψ) →
-          ( Σ (y : A t) , (y = ext-projection-temp t))
-          [ ϕ t ↦ (a t , refl)])
-    := weak-ext-ext 
-        ( I)
-        ( ψ)
-        ( ϕ)
-        ( \ t → (Σ (y : A t) , y = ext-projection-temp t))
-        ( \ t → is-contr-codomain-based-paths (A t) (ext-projection-temp t))
-        ( \ t → (a t , refl))
+  :=
+    weak-ext-ext
+    ( I )
+    ( ψ )
+    ( ϕ )
+    ( \ t → (Σ (y : A t) , ((ext-projection-temp) t = y)))
+    ( \ t →
+      is-contr-based-paths (A t ) ((ext-projection-temp) t))
+    ( \ t → (a t , refl) )
+
+#define is-contr-ext-codomain-based-paths uses (weak-ext-ext f)
+  : is-contr
+    ( ( t : ψ) →
+      ( Σ (y : A t) , (y = ext-projection-temp t)) [ ϕ t ↦ (a t , refl)])
+  :=
+    weak-ext-ext
+    ( I)
+    ( ψ)
+    ( ϕ)
+    ( \ t → (Σ (y : A t) , y = ext-projection-temp t))
+    ( \ t → is-contr-codomain-based-paths (A t) (ext-projection-temp t))
+    ( \ t → (a t , refl))
 
 #define is-contr-based-paths-ext uses (weak-ext-ext)
   : is-contr (Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
@@ -347,10 +348,10 @@ The map that defines extension extensionality
         ((t : ψ ) → (f t = g t) [ϕ t ↦ refl]))
   :=
     total-map
-      ( (t : ψ ) → A t [ϕ t ↦ a t])
-      ( \ g → (f = g))
-      ( \ g → (t : ψ ) → (f t = g t) [ϕ t ↦ refl])
-      ( ext-htpy-eq I ψ ϕ A a f)
+    ( (t : ψ ) → A t [ϕ t ↦ a t])
+    ( \ g → (f = g))
+    ( \ g → (t : ψ ) → (f t = g t) [ϕ t ↦ refl])
+    ( ext-htpy-eq I ψ ϕ A a f)
 ```
 
 The total bundle version of extension extensionality
@@ -370,14 +371,14 @@ The total bundle version of extension extensionality
                (ext-ext-weak-ext-ext-map I ψ ϕ A a f)
   :=
     is-equiv-are-contr
-      ((Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]), (f = g))  )
-      ( Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
+    ( Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]), (f = g)  )
+    ( Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
       ((t : ψ ) → (f t = g t) [ϕ t ↦ refl]))
-      ( is-contr-based-paths
-        ( (t : ψ ) → A t [ϕ t ↦ a t])
-        ( f ))
-      ( is-contr-based-paths-ext weak-ext-ext I ψ ϕ A a f)
-      ( ext-ext-weak-ext-ext-map I ψ ϕ A a f)
+    ( is-contr-based-paths
+      ( (t : ψ ) → A t [ϕ t ↦ a t])
+      ( f ))
+    ( is-contr-based-paths-ext weak-ext-ext I ψ ϕ A a f)
+    ( ext-ext-weak-ext-ext-map I ψ ϕ A a f)
 ```
 
 Finally, using equivalences between families of equivalences and bundles of
@@ -412,7 +413,7 @@ extension extensionality that we get by extraccting the fiberwise equivalence.
 ```rzk title="RS17 Proposition 4.8(i)"
 #define ext-ext-weak-ext-ext
   (weak-ext-ext : WeakExtExt)
-   :  ExtExt
+  :  ExtExt
   := \ I ψ ϕ A a f g →
       ext-ext-weak-ext-ext' weak-ext-ext I ψ ϕ A a f g
 ```
@@ -478,25 +479,28 @@ equivalences of extension types. For simplicity, we extend from `#!rzk BOT`.
               ( b)
               ( \ t → second (second (second (famequiv t))) (b t))))))
 ```
-We have a homotopy extension property. 
 
-The following code is another instantiation of casting, necessary for some arguments below. 
+We have a homotopy extension property.
+
+The following code is another instantiation of casting, necessary for some
+arguments below.
 
 ```rzk
 #define restrict
-    ( I : CUBE)
-    ( ψ : I → TOPE)
-    ( ϕ : ψ → TOPE)
-    ( A : ψ → U) 
-    ( a : (t : ϕ) → A t) 
-    ( f : (t : ψ) → A t [ϕ t ↦ a t]) 
-    : (t : ψ ) → A t
-    := f
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A : ψ → U)
+  ( a : (t : ϕ) → A t)
+  ( f : (t : ψ) → A t [ϕ t ↦ a t])
+  : (t : ψ ) → A t
+  := f
 
 ```
 
-The homotopy extension property follows from a straightforward application of the axiom of choice
-to the point of contraction for weak extension extensionality. 
+The homotopy extension property follows from a straightforward application of
+the axiom of choice to the point of contraction for weak extension
+extensionality.
 
 ```rzk title="RS17 Proposition 4.10"
 #define htpy-ext-property
@@ -506,29 +510,28 @@ to the point of contraction for weak extension extensionality.
   ( ϕ : ψ → TOPE)
   ( A : ψ → U)
   ( b : (t : ψ) → A t)
-  ( a : (t : ϕ) → A t) 
-  ( e : (t : ϕ) → a t = b t) 
-  : Σ (a' : (t : ψ) → A t [ϕ t ↦ a t]) , 
+  ( a : (t : ϕ) → A t)
+  ( e : (t : ϕ) → a t = b t)
+  : Σ (a' : (t : ψ) → A t [ϕ t ↦ a t]) ,
       ((t : ψ) → (restrict I ψ ϕ A a a' t = b t) [ϕ t ↦ e t])
-  := 
-    first 
-    ( axiom-choice 
+  :=
+    first
+    ( axiom-choice
       ( I)
-      ( ψ) 
-      ( ϕ) 
-      ( A) 
+      ( ψ)
+      ( ϕ)
+      ( A)
       ( \ t y → y = b t)
-      ( a) 
-      ( e))  
-    ( first 
-      ( weak-ext-ext 
+      ( a)
+      ( e))
+    ( first
+      ( weak-ext-ext
         ( I)
         ( ψ)
         ( ϕ)
         ( \ t → (Σ (y : A t) , y = b t))
-        ( \ t → is-contr-codomain-based-paths 
+        ( \ t → is-contr-codomain-based-paths
                 ( A t)
                 ( b t))
         ( \ t → ( a t , e t) )))
 ```
-