From d87538ecdf0eb3d1495950cd647a70f6ee16f68d Mon Sep 17 00:00:00 2001
From: Jonathan Campbell <jonathan@pop-os.localdomain>
Date: Tue, 26 Sep 2023 09:54:54 +0200
Subject: [PATCH 01/16] saving off some work

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

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index ec874972..57df547a 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -536,7 +536,10 @@ extensionality.
         ( \ t → ( a t , e t) )))
 ```
 
-In an extension type of a dependent type that is pointwise contractible, then we have an inhabitant of the extension type witnessing the contraction, at every inhabitant of the base, of each point in the fiber to the center of the fiber. Both directions of this statement will be needed. 
+In an extension type of a dependent type that is pointwise contractible, then we
+have an inhabitant of the extension type witnessing the contraction, at every
+inhabitant of the base, of each point in the fiber to the center of the fiber.
+Both directions of this statement will be needed.
 
 ```rzk
 
@@ -558,16 +561,16 @@ In an extension type of a dependent type that is pointwise contractible, then we
   ( a : (t : ϕ ) → A t)
   ( is-contr-fiberwise-A : (t : ψ ) → is-contr ( A t))
   : (t : ϕ ) → (a t = first (is-contr-fiberwise-A t))
-  :=  \ t → 
+  :=  \ t →
           rev
             ( A t )
             ( first (is-contr-fiberwise-A t) )
-            ( a t) -- 
+            ( a t) --
             ( second (is-contr-fiberwise-A t) (a t))
 
 ```
 
-```rzk 
+```rzk
 
 #define first-4-11
   (weak-ext-ext : WeakExtExt)
@@ -578,11 +581,11 @@ In an extension type of a dependent type that is pointwise contractible, then we
   ( a : (t : ϕ ) → A t)
   (is-contr-fiberwise-A : (t : ψ ) → is-contr (A t))
   : Σ (a' : (t : ψ ) → A t [ϕ t ↦ a t]),
-           ((t : ψ ) → 
-            (restrict I ψ ϕ A a a' t = 
+           ((t : ψ ) →
+            (restrict I ψ ϕ A a a' t =
               first (is-contr-fiberwise-A t))
               [ϕ t ↦ codomain-eq-ext-is-contr I ψ ϕ A a is-contr-fiberwise-A t] )
-  := 
+  :=
     htpy-ext-property
     ( weak-ext-ext)
     ( I )
@@ -605,9 +608,34 @@ In an extension type of a dependent type that is pointwise contractible, then we
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
   (is-contr-fiberwise-A : (t : ψ ) → is-contr (A t))
   : (t : ψ ) → f t = (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t
-  := \ t → eq-is-contr 
+  := \ t → eq-is-contr
               ( A t)
               ( is-contr-fiberwise-A t)
               ( f t )
               ( restrict I ψ ϕ A a (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t)
 ```
+
+```rzk
+#define third-4-11
+  ( weak-ext-ext : WeakExtExt)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A : ψ → U)
+  ( is-fiberwise-contr : (t : ψ ) → is-contr (A t))
+  ( a : (t : ϕ ) → A t)
+  ( f : (t : ψ ) → A t [ϕ t ↦ a t])
+  ( a' : (t : ψ ) → A t [ϕ t ↦ a t])
+  ( c : (t : ψ ) → (f t = a' t))
+  : (t : ψ ) → (c t = refl)
+  :=  \ t →
+    all-paths-eq-is-contr
+      ( A t)
+      ( is-fiberwise-contr t)
+      ( f t)
+      ( a' t)
+      ( c t)
+      ( refl _)
+
+
+```

From f9bc6ad1887fe79f805db44bab90eae9bb628d5a Mon Sep 17 00:00:00 2001
From: Jonathan Campbell <jonathan@pop-os.localdomain>
Date: Tue, 26 Sep 2023 10:29:21 +0200
Subject: [PATCH 02/16] some fiddling with the proof of 4.11

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

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 57df547a..4b9cb002 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -627,7 +627,7 @@ Both directions of this statement will be needed.
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
   ( a' : (t : ψ ) → A t [ϕ t ↦ a t])
   ( c : (t : ψ ) → (f t = a' t))
-  : (t : ψ ) → (c t = refl)
+  : (t : ψ ) → (c t =_{f t = a' t} refl)
   :=  \ t →
     all-paths-eq-is-contr
       ( A t)
@@ -635,7 +635,7 @@ Both directions of this statement will be needed.
       ( f t)
       ( a' t)
       ( c t)
-      ( refl _)
+      ( refl)
 
 
 ```

From 6b45d9626fdc48806987df1377b12c65c30d5ebd Mon Sep 17 00:00:00 2001
From: Jonathan Campbell <jonathan@pop-os.localdomain>
Date: Thu, 28 Sep 2023 10:43:50 +0200
Subject: [PATCH 03/16] more helper functions

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

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 4b9cb002..7f862801 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -498,9 +498,30 @@ arguments below.
 
 ```
 
-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 has the following signature. We state this
+separately since below we will will both show that this follows from extension
+extensionality, but we will also show that extension extensionality follows from
+the homotopy extension property together with extra hypotheses.
+
+```rzk
+#define HtpyExtProp
+  : U
+  :=
+    ( 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])
+
+```
+
+If we assume weak extension extensionality, then then 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
@@ -570,6 +591,9 @@ Both directions of this statement will be needed.
 
 ```
 
+The below gives us the inhabitant $(a', e')$ from the first part of the proof of
+RS Prop 4.11.
+
 ```rzk
 
 #define first-4-11
@@ -597,6 +621,8 @@ Both directions of this statement will be needed.
     ( codomain-eq-ext-is-contr I ψ ϕ A a is-contr-fiberwise-A )
 ```
 
+This gives us the inhabitant $c$
+
 ```rzk
 #define second-4-11
   (weak-ext-ext : WeakExtExt)
@@ -608,13 +634,16 @@ Both directions of this statement will be needed.
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
   (is-contr-fiberwise-A : (t : ψ ) → is-contr (A t))
   : (t : ψ ) → f t = (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t
-  := \ t → eq-is-contr
-              ( A t)
-              ( is-contr-fiberwise-A t)
-              ( f t )
-              ( restrict I ψ ϕ A a (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t)
+  := \ t →
+      eq-is-contr
+      ( A t)
+      ( is-contr-fiberwise-A t)
+      ( f t )
+      ( restrict I ψ ϕ A a (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t)
 ```
 
+And below proves that $c(t) = refl$.
+
 ```rzk
 #define third-4-11
   ( weak-ext-ext : WeakExtExt)
@@ -627,15 +656,83 @@ Both directions of this statement will be needed.
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
   ( a' : (t : ψ ) → A t [ϕ t ↦ a t])
   ( c : (t : ψ ) → (f t = a' t))
-  : (t : ψ ) → (c t =_{f t = a' t} refl)
+  : (t : ϕ ) → (refl =_{f t = a' t} c t)
   :=  \ t →
     all-paths-eq-is-contr
-      ( A t)
-      ( is-fiberwise-contr t)
-      ( f t)
-      ( a' t)
-      ( c t)
-      ( refl)
+    ( A t)
+    ( is-fiberwise-contr t)
+    ( f t)
+    ( a' t)
+    ( refl )
+    ( c t )
+
+
+```
 
+```rzk
+#define fourth-4-11
+  ( weak-ext-ext : WeakExtExt)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A : ψ → U)
+  ( is-contr-fiberwise-A : (t : ψ ) → is-contr (A t))
+  ( b : (t : ψ) → A t)
+  ( a : (t : ϕ) → A t)
+  ( f : (t : ψ ) → A t [ϕ t ↦ a t])
+  : (t : ψ ) → (f t = (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t)[ϕ t ↦ refl]
+  :=
+  first(
+    htpy-ext-property
+    ( weak-ext-ext) --- weak ext ext
+    ( I )  --- I
+    ( ψ ) --- psi
+    ( ϕ )  --- phi
+    ( \ t → f t = first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A) t) --- ft = a't, i.e. A
+    ( second-4-11
+      ( weak-ext-ext)
+      ( I)
+      ( ψ)
+      ( ϕ)
+      ( A)
+      ( a)
+      ( f)
+      ( is-contr-fiberwise-A )
+    )
+    ( \ t → refl )
+    ( third-4-11
+      ( weak-ext-ext )
+      ( I )
+      ( ψ )
+      ( ϕ )
+      ( A )
+      ( is-contr-fiberwise-A)
+      ( a )
+      ( f )
+      (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A))
+      (second-4-11
+      ( weak-ext-ext)
+      ( I)
+      ( ψ)
+      ( ϕ)
+      ( A)
+      ( a)
+      ( f)
+      ( is-contr-fiberwise-A )) -- c
+    ))
+
+```
+
+The name of the following type is cumbersome. It says that the weak extension
+extensionality statement follows from RS Prop 4.8 (ii), which is encoded as
+`eq-ext-htpy` combined with the homotopy extension property,
+`htpy-ext-property`. The proposition appears as RS Proposition 4.11
+
+```rzk
+#define weak-ext-ext-from-eq-ext-htpy-htpy-ext-property
+ (extext : ExtExt)
+ (htpy-ext-prop : HtpyExtProp)
+ : WeakExtExt
+  := \ I ψ ϕ A is-locally-contr-A a →
 
 ```

From 9c96055e5b190e2d6043347ac44ec4c2517b8b6f Mon Sep 17 00:00:00 2001
From: Jonathan Campbell <jonathan@pop-os.localdomain>
Date: Thu, 28 Sep 2023 10:45:56 +0200
Subject: [PATCH 04/16] edits

---
 src/simplicial-hott/04-extension-types.rzk.md | 14 --------------
 1 file changed, 14 deletions(-)

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 7f862801..830310df 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -722,17 +722,3 @@ And below proves that $c(t) = refl$.
     ))
 
 ```
-
-The name of the following type is cumbersome. It says that the weak extension
-extensionality statement follows from RS Prop 4.8 (ii), which is encoded as
-`eq-ext-htpy` combined with the homotopy extension property,
-`htpy-ext-property`. The proposition appears as RS Proposition 4.11
-
-```rzk
-#define weak-ext-ext-from-eq-ext-htpy-htpy-ext-property
- (extext : ExtExt)
- (htpy-ext-prop : HtpyExtProp)
- : WeakExtExt
-  := \ I ψ ϕ A is-locally-contr-A a →
-
-```

From f638c5ac7e9d100b8a93070b0648c496c6c901e0 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 28 Sep 2023 16:29:47 +0200
Subject: [PATCH 05/16] delete this, as suggested by Emily

---
 src/hott/06-contractible.rzk.md | 18 ------------------
 1 file changed, 18 deletions(-)

diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md
index f33ed30c..02f4a5e5 100644
--- a/src/hott/06-contractible.rzk.md
+++ b/src/hott/06-contractible.rzk.md
@@ -412,24 +412,6 @@ separate hypothesis.
 
 ```
 
-For future reference we add a variable we can assume.
-
-```rzk
-#assume weakfunext : WeakFunExt
-```
-
-Whenever a definition (implicitly) uses function extensionality, we write
-`#!rzk uses (weakfunext)`.
-
-```rzk
-#def call-weakfunext uses (weakfunext)
-  ( A : U )
-  ( C : A → U)
-  ( f : (a : A) → is-contr (C a) )
-  : (is-contr ( (a : A) → C a ))
-  := weakfunext A C f
-```
-
 ## Singleton induction
 
 A type is contractible if and only if it has singleton induction.

From 8419403e8fea5b4322f2afdb271069c5345d2a82 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 28 Sep 2023 17:41:21 +0200
Subject: [PATCH 06/16] weakfunext-funext

---
 src/hott/06-contractible.rzk.md | 39 +++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md
index 02f4a5e5..a469ffe3 100644
--- a/src/hott/06-contractible.rzk.md
+++ b/src/hott/06-contractible.rzk.md
@@ -407,11 +407,50 @@ separate hypothesis.
 #def WeakFunExt : U
   :=
     ( A : U ) → (C : A → U) →
+    -- TODO: rename f (also below)?
     (f : (a : A) → is-contr (C a) ) →
     (is-contr ( (a : A) → C a ))
 
 ```
 
+Weak function extensionality implies function extensionality.
+
+
+```rzk
+-- TODO: delete
+#assume hole : (A : U) → A
+
+#def funext-weakfunext
+  ( weakfunext : WeakFunExt )
+  : FunExt
+  := hole FunExt
+```
+
+```rzk
+-- TODO: better name? or inline this?
+#def map-weakfunext-funext
+  (A : U)
+  (C : A → U)
+  (f : (a : A) → is-contr (C a))
+  : (a : A) → C a
+  :=
+  \ a → first (f a)
+
+#def weakfunext-funext
+  (funext : FunExt)
+  : WeakFunExt
+  :=
+  ( \ A → \ C → \ f →
+    ( map-weakfunext-funext A C f ,
+      ( \ (g : (a : A) → C a) →
+        ( eq-htpy funext
+          ( A)
+          ( C)
+          ( map-weakfunext-funext A C f)
+          ( g)
+          ( \ a → second (f a) (g a))))))
+```
+
 ## Singleton induction
 
 A type is contractible if and only if it has singleton induction.

From 2b38f9035151c06ddb9818523730e1e376f531a0 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 28 Sep 2023 17:52:57 +0200
Subject: [PATCH 07/16] name idea

---
 src/hott/06-contractible.rzk.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md
index a469ffe3..b716fe3c 100644
--- a/src/hott/06-contractible.rzk.md
+++ b/src/hott/06-contractible.rzk.md
@@ -407,7 +407,7 @@ separate hypothesis.
 #def WeakFunExt : U
   :=
     ( A : U ) → (C : A → U) →
-    -- TODO: rename f (also below)?
+    -- TODO: rename f to is-contr-C (also below)?
     (f : (a : A) → is-contr (C a) ) →
     (is-contr ( (a : A) → C a ))
 

From 4132c1b6d42e95b19ef31508e69373915c6338e6 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Fri, 29 Sep 2023 11:44:12 +0200
Subject: [PATCH 08/16] polish

---
 src/hott/06-contractible.rzk.md | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md
index b716fe3c..f67e3ad4 100644
--- a/src/hott/06-contractible.rzk.md
+++ b/src/hott/06-contractible.rzk.md
@@ -426,6 +426,8 @@ Weak function extensionality implies function extensionality.
   := hole FunExt
 ```
 
+Function extensionality implies weak function extensionality.
+
 ```rzk
 -- TODO: better name? or inline this?
 #def map-weakfunext-funext
@@ -440,15 +442,15 @@ Weak function extensionality implies function extensionality.
   (funext : FunExt)
   : WeakFunExt
   :=
-  ( \ A → \ C → \ f →
-    ( map-weakfunext-funext A C f ,
-      ( \ (g : (a : A) → C a) →
-        ( eq-htpy funext
-          ( A)
-          ( C)
-          ( map-weakfunext-funext A C f)
-          ( g)
-          ( \ a → second (f a) (g a))))))
+  \ A C f →
+  ( map-weakfunext-funext A C f ,
+    ( \ (g : (a : A) → C a) →
+      ( eq-htpy funext
+        ( A)
+        ( C)
+        ( map-weakfunext-funext A C f)
+        ( g)
+        ( \ a → second (f a) (g a)))))
 ```
 
 ## Singleton induction

From c4405ed08206ab168068744b89cff3a752fc967c Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Fri, 29 Sep 2023 12:22:35 +0200
Subject: [PATCH 09/16] clean up

---
 src/hott/06-contractible.rzk.md | 31 ++++++++-----------------------
 1 file changed, 8 insertions(+), 23 deletions(-)

diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md
index f67e3ad4..2570038c 100644
--- a/src/hott/06-contractible.rzk.md
+++ b/src/hott/06-contractible.rzk.md
@@ -407,50 +407,35 @@ separate hypothesis.
 #def WeakFunExt : U
   :=
     ( A : U ) → (C : A → U) →
-    -- TODO: rename f to is-contr-C (also below)?
-    (f : (a : A) → is-contr (C a) ) →
+    (is-contr-C : (a : A) → is-contr (C a) ) →
     (is-contr ( (a : A) → C a ))
 
 ```
 
-Weak function extensionality implies function extensionality.
-
-
-```rzk
--- TODO: delete
-#assume hole : (A : U) → A
-
-#def funext-weakfunext
-  ( weakfunext : WeakFunExt )
-  : FunExt
-  := hole FunExt
-```
-
 Function extensionality implies weak function extensionality.
 
 ```rzk
--- TODO: better name? or inline this?
-#def map-weakfunext-funext
+#def map-for-weakfunext
   (A : U)
   (C : A → U)
-  (f : (a : A) → is-contr (C a))
+  (is-contr-C : (a : A) → is-contr (C a))
   : (a : A) → C a
   :=
-  \ a → first (f a)
+  \ a → first (is-contr-C a)
 
 #def weakfunext-funext
   (funext : FunExt)
   : WeakFunExt
   :=
-  \ A C f →
-  ( map-weakfunext-funext A C f ,
+  \ A C is-contr-C →
+  ( map-for-weakfunext A C is-contr-C ,
     ( \ (g : (a : A) → C a) →
       ( eq-htpy funext
         ( A)
         ( C)
-        ( map-weakfunext-funext A C f)
+        ( map-for-weakfunext A C is-contr-C)
         ( g)
-        ( \ a → second (f a) (g a)))))
+        ( \ a → second (is-contr-C a) (g a)))))
 ```
 
 ## Singleton induction

From 77fc08def4f80864e8a133ba28380bd77ba5f454 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Fri, 29 Sep 2023 12:27:30 +0200
Subject: [PATCH 10/16] remove unusual annotation

---
 src/hott/06-contractible.rzk.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md
index 2570038c..1d5e0ecf 100644
--- a/src/hott/06-contractible.rzk.md
+++ b/src/hott/06-contractible.rzk.md
@@ -429,7 +429,7 @@ Function extensionality implies weak function extensionality.
   :=
   \ A C is-contr-C →
   ( map-for-weakfunext A C is-contr-C ,
-    ( \ (g : (a : A) → C a) →
+    ( \ g →
       ( eq-htpy funext
         ( A)
         ( C)

From 71f03be4e5610bbe3247c30b1b9dbbc8ff5db133 Mon Sep 17 00:00:00 2001
From: Jonathan Campbell <jonathan@pop-os.localdomain>
Date: Fri, 29 Sep 2023 19:49:24 +0200
Subject: [PATCH 11/16] changed some names to more descriptive ones

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

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 830310df..a49c8ecc 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -244,8 +244,7 @@ We refer to another form as an "extension extensionality" axiom.
     ( ϕ : ψ → TOPE) →
     ( A : ψ → U) →
     ( a : (t : ϕ) → A t) →
-    ( f : (t : ψ) → A t [ϕ t ↦ a t]) →
-    ( g : (t : ψ) → A t [ϕ t ↦ a t]) →
+    ( f g : (t : ψ) → A t [ϕ t ↦ a t]) →
     is-equiv
       ( f = g)
       ( (t : ψ) → (f t = g t) [ϕ t ↦ refl])
@@ -504,7 +503,7 @@ extensionality, but we will also show that extension extensionality follows from
 the homotopy extension property together with extra hypotheses.
 
 ```rzk
-#define HtpyExtProp
+#define HtpyExtProperty
   : U
   :=
     ( I : CUBE) →
@@ -523,6 +522,34 @@ If we assume weak extension extensionality, then then 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-proprty-weak-ext-ext
+  ( weak-ext-ext : WeakExtExt)
+  : HtpyExtProperty
+  :=
+    \ I ψ ϕ A b a e →
+    first
+    ( axiom-choice
+      ( I)
+      ( ψ)
+      ( ϕ)
+      ( A)
+      ( \ t y → y = b t)
+      ( a)
+      ( e))
+    ( first
+      ( weak-ext-ext
+        ( I)
+        ( ψ)
+        ( ϕ)
+        ( \ t → (Σ (y : A t) , y = b t))
+        ( \ t → is-contr-codomain-based-paths
+                ( A t)
+                ( b t))
+        ( \ t → ( a t , e t) )))
+
+```
+
 ```rzk title="RS17 Proposition 4.10"
 #define htpy-ext-property
   ( weak-ext-ext : WeakExtExt)
@@ -591,13 +618,18 @@ Both directions of this statement will be needed.
 
 ```
 
-The below gives us the inhabitant $(a', e')$ from the first part of the proof of
-RS Prop 4.11.
+The below gives us the inhabitant
+$(a', e') : \sum_{\left\langle\prod_{t : I|\psi} A (t) \biggr|^\phi_a\right\rangle} \left\langle \prod_{t: I |\psi} a'(t) = b(t)\biggr|^\phi_e \right\rangle$
+from the first part of the proof of RS Prop 4.11. It amounts to the fact that
+parameterized contractibility, i.e. $A : \{t : I | \psi\} → \mathcal{U}$ such
+that each $A(t)$ is contractible, implies the hypotheses of the homotopy
+extension property are satisfied, and so assuming homotopy extension property,
+we are entitled to the conclusion.
 
 ```rzk
 
-#define first-4-11
-  (weak-ext-ext : WeakExtExt)
+#define htpy-ext-prop-is-fiberwise-contr
+  (htpy-ext-prop : HtpyExtProperty)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -610,22 +642,27 @@ RS Prop 4.11.
               first (is-contr-fiberwise-A t))
               [ϕ t ↦ codomain-eq-ext-is-contr I ψ ϕ A a is-contr-fiberwise-A t] )
   :=
-    htpy-ext-property
-    ( weak-ext-ext)
-    ( I )
-    ( ψ )
-    ( ϕ )
-    ( A )
+    htpy-ext-prop
+    ( I)
+    ( ψ)
+    ( ϕ)
+    ( A)
     (\ t →  first (is-contr-fiberwise-A t))
-    ( a )
-    ( codomain-eq-ext-is-contr I ψ ϕ A a is-contr-fiberwise-A )
+    ( a)
+    ( codomain-eq-ext-is-contr I ψ ϕ A a is-contr-fiberwise-A)
 ```
 
-This gives us the inhabitant $c$
+The two expressions below give us the inhabitant
+$c : \prod_{t: I | \psi} f(t) = a' (t)$ used in the proof of RS Proposition 4.11
+
+```rzk
+
+
+```
 
 ```rzk
 #define second-4-11
-  (weak-ext-ext : WeakExtExt)
+  (htpy-ext-prop : HtpyExtProperty)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -633,20 +670,22 @@ This gives us the inhabitant $c$
   ( a : (t : ϕ ) → A t)
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
   (is-contr-fiberwise-A : (t : ψ ) → is-contr (A t))
-  : (t : ψ ) → f t = (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t
+  : (t : ψ ) →
+      f t = (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t
   := \ t →
       eq-is-contr
       ( A t)
       ( is-contr-fiberwise-A t)
       ( f t )
-      ( restrict I ψ ϕ A a (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t)
+      ( restrict I ψ ϕ A a
+         (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t)
 ```
 
 And below proves that $c(t) = refl$.
 
 ```rzk
 #define third-4-11
-  ( weak-ext-ext : WeakExtExt)
+ -- ( weak-ext-ext : WeakExtExt)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -671,26 +710,25 @@ And below proves that $c(t) = refl$.
 
 ```rzk
 #define fourth-4-11
-  ( weak-ext-ext : WeakExtExt)
+  (htpy-ext-prop : HtpyExtProperty)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
   ( A : ψ → U)
   ( is-contr-fiberwise-A : (t : ψ ) → is-contr (A t))
-  ( b : (t : ψ) → A t)
+ -- ( b : (t : ψ) → A t)
   ( a : (t : ϕ) → A t)
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
-  : (t : ψ ) → (f t = (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t)[ϕ t ↦ refl]
+  : (t : ψ ) → (f t = (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t)[ϕ t ↦ refl]
   :=
   first(
-    htpy-ext-property
-    ( weak-ext-ext) --- weak ext ext
-    ( I )  --- I
-    ( ψ ) --- psi
-    ( ϕ )  --- phi
-    ( \ t → f t = first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A) t) --- ft = a't, i.e. A
+    htpy-ext-prop
+    ( I )
+    ( ψ )
+    ( ϕ )
+    ( \ t → f t = first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A) t) --- ft = a't, i.e. A
     ( second-4-11
-      ( weak-ext-ext)
+      ( htpy-ext-prop)
       ( I)
       ( ψ)
       ( ϕ)
@@ -701,7 +739,6 @@ And below proves that $c(t) = refl$.
     )
     ( \ t → refl )
     ( third-4-11
-      ( weak-ext-ext )
       ( I )
       ( ψ )
       ( ϕ )
@@ -709,16 +746,16 @@ And below proves that $c(t) = refl$.
       ( is-contr-fiberwise-A)
       ( a )
       ( f )
-      (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A))
+      (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A))
       (second-4-11
-      ( weak-ext-ext)
+      ( htpy-ext-prop)
       ( I)
       ( ψ)
       ( ϕ)
       ( A)
       ( a)
       ( f)
-      ( is-contr-fiberwise-A )) -- c
+      ( is-contr-fiberwise-A ))
     ))
 
 ```

From 362ae4bc4a6688995bf8864d241402a6eeca0b2d Mon Sep 17 00:00:00 2001
From: Jonathan Campbell <jonathan@pop-os.localdomain>
Date: Fri, 29 Sep 2023 20:35:36 +0200
Subject: [PATCH 12/16] finished with the proof of 4.11

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

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index a49c8ecc..9aa6c35e 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -244,7 +244,8 @@ We refer to another form as an "extension extensionality" axiom.
     ( ϕ : ψ → TOPE) →
     ( A : ψ → U) →
     ( a : (t : ϕ) → A t) →
-    ( f g : (t : ψ) → A t [ϕ t ↦ a t]) →
+    ( f  : (t : ψ) → A t [ϕ t ↦ a t]) →
+    ( g : (t : ψ ) → A t [ϕ t ↦ a t]) →
     is-equiv
       ( f = g)
       ( (t : ψ) → (f t = g t) [ϕ t ↦ refl])
@@ -264,6 +265,24 @@ We refer to another form as an "extension extensionality" axiom.
   := (ext-htpy-eq I ψ ϕ A a f g , extext I ψ ϕ A a f g)
 ```
 
+For readability of code, it is useful to have the forward map of extension
+extensionality available. In fact, sometimes only this implication is needed.
+
+```rzk title = "The equality provided by extension extensionality"
+#def EqExtExt
+  : U
+  :=
+  ( I : CUBE) →
+  ( ψ : I → TOPE) →
+  ( ϕ : ψ → TOPE) →
+  ( A : ψ → U) →
+  ( a : (t : ϕ) → A t) →
+  ( f  : (t : ψ) → A t [ϕ t ↦ a t]) →
+  ( g  : (t : ψ) → A t [ϕ t ↦ a t]) →
+  ( (t : ψ ) → (f t = g t) [ϕ t ↦ refl]) →
+  ( f = g)
+```
+
 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
@@ -652,16 +671,13 @@ we are entitled to the conclusion.
     ( codomain-eq-ext-is-contr I ψ ϕ A a is-contr-fiberwise-A)
 ```
 
-The two expressions below give us the inhabitant
-$c : \prod_{t: I | \psi} f(t) = a' (t)$ used in the proof of RS Proposition 4.11
-
-```rzk
-
-
-```
+The expression below give us the inhabitant
+$c : \prod_{t: I | \psi} f(t) = a' (t)$ used in the proof of RS Proposition
+4.11. It follows from a more general statement about the contractibility of
+identity types, but it is unclear if that generality is needed.
 
 ```rzk
-#define second-4-11
+#define RS-4-11-c
   (htpy-ext-prop : HtpyExtProperty)
   ( I : CUBE)
   ( ψ : I → TOPE)
@@ -681,10 +697,11 @@ $c : \prod_{t: I | \psi} f(t) = a' (t)$ used in the proof of RS Proposition 4.11
          (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t)
 ```
 
-And below proves that $c(t) = refl$.
+And below proves that $c(t) = refl$. Again, this is a consequence of a slightly
+more general statement.
 
 ```rzk
-#define third-4-11
+#define RS-4-11-c-is-refl
  -- ( weak-ext-ext : WeakExtExt)
   ( I : CUBE)
   ( ψ : I → TOPE)
@@ -708,8 +725,11 @@ And below proves that $c(t) = refl$.
 
 ```
 
+Given the $a'$ produced above, the following gives an inhabitant of
+$\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\rangle$
+
 ```rzk
-#define fourth-4-11
+#define is-fiberwise-contr-ext-is-fiberwise-contr
   (htpy-ext-prop : HtpyExtProperty)
   ( I : CUBE)
   ( ψ : I → TOPE)
@@ -719,43 +739,72 @@ And below proves that $c(t) = refl$.
  -- ( b : (t : ψ) → A t)
   ( a : (t : ϕ) → A t)
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
-  : (t : ψ ) → (f t = (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t)[ϕ t ↦ refl]
+  : (t : ψ ) →
+      (f t = (first
+              (htpy-ext-prop-is-fiberwise-contr
+                htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t)[ϕ t ↦ refl]
   :=
   first(
     htpy-ext-prop
     ( I )
     ( ψ )
     ( ϕ )
-    ( \ t → f t = first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A) t) --- ft = a't, i.e. A
-    ( second-4-11
-      ( htpy-ext-prop)
+    ( \ t → f t = first
+                  (htpy-ext-prop-is-fiberwise-contr
+                    htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A) t)
+    ( RS-4-11-c
+      htpy-ext-prop I ψ ϕ A a f is-contr-fiberwise-A)
+    ( \ t → refl )
+    ( RS-4-11-c-is-refl
       ( I)
       ( ψ)
       ( ϕ)
       ( A)
-      ( a)
-      ( f)
-      ( is-contr-fiberwise-A )
-    )
-    ( \ t → refl )
-    ( third-4-11
-      ( I )
-      ( ψ )
-      ( ϕ )
-      ( A )
       ( is-contr-fiberwise-A)
       ( a )
       ( f )
-      (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A))
-      (second-4-11
-      ( htpy-ext-prop)
+      ( first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A))
+      ( RS-4-11-c
+        ( htpy-ext-prop)
+        ( I)
+        ( ψ)
+        ( ϕ)
+        ( A)
+        ( a)
+        ( f)
+        ( is-contr-fiberwise-A ))))
+
+```
+
+```rzk
+#define weak-ext-ext-from-eq-ext-htpy-htpy-ext-property
+ (eq-ext-ext : EqExtExt)
+ (htpy-ext-prop : HtpyExtProperty)
+ : WeakExtExt
+  := \ I ψ ϕ A is-contr-fiberwise-A a →
+    (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A),
+     \ f →
+      rev
+      ( (t : ψ ) → A t [ϕ t ↦ a t])
+      ( f )
+      ( first (htpy-ext-prop-is-fiberwise-contr
+                htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A))
+      (eq-ext-ext
       ( I)
-      ( ψ)
-      ( ϕ)
+      ( ψ )
+      ( ϕ )
       ( A)
       ( a)
       ( f)
-      ( is-contr-fiberwise-A ))
-    ))
-
+      ( first (htpy-ext-prop-is-fiberwise-contr
+                htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A))
+      ( is-fiberwise-contr-ext-is-fiberwise-contr
+        ( htpy-ext-prop)
+        ( I)
+        ( ψ )
+        ( ϕ )
+        ( A)
+        ( is-contr-fiberwise-A)
+        ( a)
+        ( f))))
 ```

From 294c39a9bf5af2c72cf38398651e4ba749c5f41f Mon Sep 17 00:00:00 2001
From: Nima Rasekh <rasekh@mpim-bonn.mpg.de>
Date: Fri, 29 Sep 2023 23:27:23 +0200
Subject: [PATCH 13/16] Morphisms of Product Types

Added Section to file 5 characterizing morphisms in product types as products of morphims
---
 src/simplicial-hott/05-segal-types.rzk.md | 49 +++++++++++++++++++++++
 1 file changed, 49 insertions(+)

diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index e0aaf210..079d45ae 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -1772,3 +1772,52 @@ The cofibration Λ²₁ → Δ² is inner anodyne
         ( is-segal-A)
         ( h^ A h))
 ```
+
+## Products of Segal Types
+
+This is an additional section which describes morphisms in products of types as products of morphisms.
+It is implicitly stated in Proposition 8.21.
+
+```rzk
+#section morphisms-of-products-is-products-of-morphisms
+#variables A B : U
+#variable p : ( product A B )
+#variable p' : ( product A B )
+
+#def morphism-in-product-to-product-of-morphism
+  : hom ( product A B ) p p' →
+    product ( hom A ( first p ) ( first p' ) ) ( hom B ( second p ) ( second p' ) )
+  :=  \ f → ( \ ( t : Δ¹ ) → first ( f t ) , \ ( t : Δ¹ ) → second ( f t ) )
+
+#def product-of-morphism-to-morphism-in-product
+  : product ( hom A ( first p ) ( first p' ) ) ( hom B ( second p ) ( second p' ) ) →
+    hom ( product A B ) p p'
+  := \ ( f , g ) ( t : Δ¹ ) → ( f t , g t )
+
+#def morphisms-in-product-to-product-of-morphism-to-morphism-in-product-is-id
+  : ( f :  product ( hom A ( first p ) ( first p' ) ) ( hom B ( second p ) ( second p' ) ) ) →
+    ( morphism-in-product-to-product-of-morphism )
+    ( ( product-of-morphism-to-morphism-in-product )
+      f ) = f
+  := \ f → refl
+
+#def product-of-morphism-to-morphisms-in-product-to-product-of-morphism-is-id
+  : ( f :  hom ( product A B ) p p' ) →
+    ( product-of-morphism-to-morphism-in-product )
+    ( ( morphism-in-product-to-product-of-morphism )
+      f ) = f
+  := \ f → refl
+
+#def morphism-in-product-equiv-product-of-morphism
+  : Equiv
+    ( hom ( product A B ) p p' )
+    ( product ( hom A ( first p ) ( first p' ) ) ( hom B ( second p ) ( second p' ) ) )
+  :=
+    ( ( morphism-in-product-to-product-of-morphism ) ,
+      ( ( ( product-of-morphism-to-morphism-in-product ) ,
+          ( product-of-morphism-to-morphisms-in-product-to-product-of-morphism-is-id ) ) ,
+        ( ( product-of-morphism-to-morphism-in-product ) ,
+          ( morphisms-in-product-to-product-of-morphism-to-morphism-in-product-is-id ) ) ) )
+
+#end morphisms-of-products-is-products-of-morphisms
+```

From b5f97aec2a580f5b32e7e894c4d24e9feaa15b4d Mon Sep 17 00:00:00 2001
From: emilyriehl <emilyriehl@math.jhu.edu>
Date: Sat, 30 Sep 2023 11:38:58 +0200
Subject: [PATCH 14/16] fix merge conflicts

---
 src/hott/08-families-of-maps.rzk.md           |   6 +-
 src/simplicial-hott/04-extension-types.rzk.md | 120 +++++++++---------
 src/simplicial-hott/08-covariant.rzk.md       |   2 +-
 3 files changed, 65 insertions(+), 63 deletions(-)

diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md
index 471b50ff..9f43f169 100644
--- a/src/hott/08-families-of-maps.rzk.md
+++ b/src/hott/08-families-of-maps.rzk.md
@@ -287,7 +287,7 @@ equivalence.
   := (family-of-equiv-total-equiv A B C f , total-equiv-family-of-equiv A B C f)
 ```
 
-## Codomain based path spaces
+## Endpoint based path spaces
 
 ```rzk title="An equivalence between the based path spaces"
 #def equiv-based-paths
@@ -297,8 +297,8 @@ equivalence.
   := total-equiv-family-equiv A (\ x → x = a) (\ x → a = x) (\ x → equiv-rev A x a)
 ```
 
-```rzk title="Codomain based path spaces are contractible"
-#def is-contr-codomain-based-paths
+```rzk title="Endpoint based path spaces are contractible"
+#def is-contr-endpoint-based-paths
   ( A : U)
   ( a : A)
   : is-contr (Σ (x : A) , x = a)
diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 9aa6c35e..bc6b80cc 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -265,22 +265,30 @@ We refer to another form as an "extension extensionality" axiom.
   := (ext-htpy-eq I ψ ϕ A a f g , extext I ψ ϕ A a f g)
 ```
 
-For readability of code, it is useful to have the forward map of extension
-extensionality available. In fact, sometimes only this implication is needed.
+For readability of code, it is useful to the function that supplies an equality
+between terms of an extension type from a pointwise equality extending refl. In
+fact, sometimes only this weaker form of the axiom is needed.
 
-```rzk title = "The equality provided by extension extensionality"
-#def EqExtExt
+```rzk
+#def NaiveExtExt
   : U
   :=
-  ( I : CUBE) →
-  ( ψ : I → TOPE) →
-  ( ϕ : ψ → TOPE) →
-  ( A : ψ → U) →
-  ( a : (t : ϕ) → A t) →
-  ( f  : (t : ψ) → A t [ϕ t ↦ a t]) →
-  ( g  : (t : ψ) → A t [ϕ t ↦ a t]) →
-  ( (t : ψ ) → (f t = g t) [ϕ t ↦ refl]) →
-  ( f = g)
+    ( I : CUBE) →
+    ( ψ : I → TOPE) →
+    ( ϕ : ψ → TOPE) →
+    ( A : ψ → U) →
+    ( a : (t : ϕ) → A t) →
+    ( f : (t : ψ) → A t [ϕ t ↦ a t]) →
+    ( g : (t : ψ) → A t [ϕ t ↦ a t]) →
+    ( (t : ψ) → (f t = g t) [ϕ t ↦ refl]) →
+    ( f = g)
+
+#def naiveextext-extext
+  ( extext : ExtExt)
+  : NaiveExtExt
+  :=
+    \ I ψ ϕ A a f g →
+      ( first (first (extext I ψ ϕ A a f g)))
 ```
 
 Weak extension extensionality implies extension extensionality; this is the
@@ -291,7 +299,7 @@ cases an extension type to a function type.
 ```rzk
 #section rs-4-8
 
-#variable  weak-ext-ext : WeakExtExt
+#variable  weakextext : WeakExtExt
 #variable  I : CUBE
 #variable  ψ : I → TOPE
 #variable  ϕ : ψ → TOPE
@@ -303,11 +311,11 @@ cases an extension type to a function type.
   : ((t : ψ ) → A t)
   := f
 
-#define is-contr-ext-based-paths uses (weak-ext-ext f)
+#define is-contr-ext-based-paths uses (weakextext f)
   : is-contr ((t : ψ ) → (Σ (y : A t) ,
               ((ext-projection-temp) t = y))[ϕ t ↦ (a t , refl)])
   :=
-    weak-ext-ext
+    weakextext
     ( I )
     ( ψ )
     ( ϕ )
@@ -316,20 +324,20 @@ cases an extension type to a function type.
       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)
+#define is-contr-ext-endpoint-based-paths uses (weakextext f)
   : is-contr
     ( ( t : ψ) →
       ( Σ (y : A t) , (y = ext-projection-temp t)) [ ϕ t ↦ (a t , refl)])
   :=
-    weak-ext-ext
+    weakextext
     ( I)
     ( ψ)
     ( ϕ)
     ( \ t → (Σ (y : A t) , y = ext-projection-temp t))
-    ( \ t → is-contr-codomain-based-paths (A t) (ext-projection-temp t))
+    ( \ t → is-contr-endpoint-based-paths (A t) (ext-projection-temp t))
     ( \ t → (a t , refl))
 
-#define is-contr-based-paths-ext uses (weak-ext-ext)
+#define is-contr-based-paths-ext uses (weakextext)
   : is-contr (Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
               (t : ψ ) → (f t = g t) [ϕ t ↦ refl])
   :=
@@ -354,7 +362,7 @@ cases an extension type to a function type.
 The map that defines extension extensionality
 
 ```rzk title="RS17 4.7"
-#define ext-ext-weak-ext-ext-map
+#define extext-weakextext-map
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -375,8 +383,8 @@ The map that defines extension extensionality
 The total bundle version of extension extensionality
 
 ```rzk
-#define ext-ext-weak-ext-ext-bundle-version
-  ( weak-ext-ext : WeakExtExt)
+#define extext-weakextext-bundle-version
+  ( weakextext : WeakExtExt)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -386,7 +394,7 @@ The total bundle version of extension extensionality
   : is-equiv ((Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]), (f = g)))
                (Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
                   ((t : ψ ) → (f t = g t) [ϕ t ↦ refl]))
-               (ext-ext-weak-ext-ext-map I ψ ϕ A a f)
+               (extext-weakextext-map I ψ ϕ A a f)
   :=
     is-equiv-are-contr
     ( Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]), (f = g)  )
@@ -395,8 +403,8 @@ The total bundle version of extension extensionality
     ( 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-ext weakextext I ψ ϕ A a f)
+    ( extext-weakextext-map I ψ ϕ A a f)
 ```
 
 Finally, using equivalences between families of equivalences and bundles of
@@ -404,16 +412,16 @@ equivalences we have that weak extension extensionality implies extension
 extensionality. The following is statement the as proved in RS17.
 
 ```rzk title="RS17 Prop 4.8(i) as proved"
-#define ext-ext-weak-ext-ext'
-  ( weak-ext-ext : WeakExtExt)
+#define extext-weakextext'
+  ( weakextext : WeakExtExt)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
   ( A : ψ → U)
   ( a : (t : ϕ ) → A t)
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
-  : (g : (t : ψ ) → A t [ϕ t ↦ a t])
-     → is-equiv
+  : (g : (t : ψ ) → A t [ϕ t ↦ a t]) →
+      is-equiv
         ( f = g)
         ( (t : ψ ) → (f t = g t) [ϕ t ↦ refl])
         ( ext-htpy-eq I ψ ϕ A a f g)
@@ -422,18 +430,18 @@ extensionality. The following is statement the as proved in RS17.
       ( \ g → (f = g) )
       ( \ g → (t : ψ ) → (f t = g t) [ϕ t ↦ refl])
       ( ext-htpy-eq I ψ ϕ A a f)
-      ( ext-ext-weak-ext-ext-bundle-version weak-ext-ext I ψ ϕ A a f)
+      ( extext-weakextext-bundle-version weakextext I ψ ϕ A a f)
 ```
 
 The following is the literal statement of weak extension extensionality implying
 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)
+#define extext-weakextext
+  (weakextext : WeakExtExt)
   :  ExtExt
   := \ I ψ ϕ A a f g →
-      ext-ext-weak-ext-ext' weak-ext-ext I ψ ϕ A a f g
+      extext-weakextext' weakextext I ψ ϕ A a f g
 ```
 
 ## Applications of extension extensionality
@@ -542,8 +550,8 @@ 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-proprty-weak-ext-ext
-  ( weak-ext-ext : WeakExtExt)
+#define htpy-ext-property-weakextext
+  ( weakextext : WeakExtExt)
   : HtpyExtProperty
   :=
     \ I ψ ϕ A b a e →
@@ -557,12 +565,12 @@ the point of contraction for weak extension extensionality.
       ( a)
       ( e))
     ( first
-      ( weak-ext-ext
+      ( weakextext
         ( I)
         ( ψ)
         ( ϕ)
         ( \ t → (Σ (y : A t) , y = b t))
-        ( \ t → is-contr-codomain-based-paths
+        ( \ t → is-contr-endpoint-based-paths
                 ( A t)
                 ( b t))
         ( \ t → ( a t , e t) )))
@@ -570,8 +578,8 @@ the point of contraction for weak extension extensionality.
 ```
 
 ```rzk title="RS17 Proposition 4.10"
-#define htpy-ext-property
-  ( weak-ext-ext : WeakExtExt)
+#define htpy-ext-prop-weakextext
+  ( weakextext : WeakExtExt)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -592,12 +600,12 @@ the point of contraction for weak extension extensionality.
       ( a)
       ( e))
     ( first
-      ( weak-ext-ext
+      ( weakextext
         ( I)
         ( ψ)
         ( ϕ)
         ( \ t → (Σ (y : A t) , y = b t))
-        ( \ t → is-contr-codomain-based-paths
+        ( \ t → is-contr-endpoint-based-paths
                 ( A t)
                 ( b t))
         ( \ t → ( a t , e t) )))
@@ -648,7 +656,7 @@ we are entitled to the conclusion.
 ```rzk
 
 #define htpy-ext-prop-is-fiberwise-contr
-  (htpy-ext-prop : HtpyExtProperty)
+  (htpy-ext-property : HtpyExtProperty)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -661,11 +669,11 @@ we are entitled to the conclusion.
               first (is-contr-fiberwise-A t))
               [ϕ t ↦ codomain-eq-ext-is-contr I ψ ϕ A a is-contr-fiberwise-A t] )
   :=
-    htpy-ext-prop
-    ( I)
-    ( ψ)
-    ( ϕ)
-    ( A)
+    htpy-ext-property
+    ( I )
+    ( ψ )
+    ( ϕ )
+    ( A )
     (\ t →  first (is-contr-fiberwise-A t))
     ( a)
     ( codomain-eq-ext-is-contr I ψ ϕ A a is-contr-fiberwise-A)
@@ -697,12 +705,11 @@ identity types, but it is unclear if that generality is needed.
          (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t)
 ```
 
-And below proves that $c(t) = refl$. Again, this is a consequence of a slightly
-more general statement.
+And below proves that `#!rzk c(t) = refl`. Again, this is a consequence of a
+slightly more general statement.
 
 ```rzk
 #define RS-4-11-c-is-refl
- -- ( weak-ext-ext : WeakExtExt)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -721,11 +728,9 @@ more general statement.
     ( a' t)
     ( refl )
     ( c t )
-
-
 ```
 
-Given the $a'$ produced above, the following gives an inhabitant of
+Given the `#rzk! a'` produced above, the following gives an inhabitant of
 $\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\rangle$
 
 ```rzk
@@ -774,11 +779,8 @@ $\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\r
         ( f)
         ( is-contr-fiberwise-A ))))
 
-```
-
-```rzk
 #define weak-ext-ext-from-eq-ext-htpy-htpy-ext-property
- (eq-ext-ext : EqExtExt)
+ (naiveextext : NaiveExtExt)
  (htpy-ext-prop : HtpyExtProperty)
  : WeakExtExt
   := \ I ψ ϕ A is-contr-fiberwise-A a →
@@ -789,7 +791,7 @@ $\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\r
       ( f )
       ( first (htpy-ext-prop-is-fiberwise-contr
                 htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A))
-      (eq-ext-ext
+      (naiveextext
       ( I)
       ( ψ )
       ( ϕ )
diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 98816b21..3841cce4 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -740,7 +740,7 @@ Now we introduce the hypothesis that A is Segal type.
     equiv-projection-contractible-fibers
       ( hom2 A a x y u f d)
       ( \ α → (Σ (v : hom A a y) , (v = d)))
-      ( \ α → is-contr-codomain-based-paths (hom A a y) d)
+      ( \ α → is-contr-endpoint-based-paths (hom A a y) d)
 
 #def is-segal-representable-dhom-from-hom2
   ( A : U)

From dbd20ff140e07c3ee97d4d8cbbd6d12eec8b4e50 Mon Sep 17 00:00:00 2001
From: Jonathan Campbell <jonathan@pop-os.localdomain>
Date: Sun, 1 Oct 2023 04:37:09 -0700
Subject: [PATCH 15/16] fixed merge issue

---
 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 f31d3b08..2bb44827 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -694,13 +694,14 @@ identity types, but it is unclear if that generality is needed.
   ( a : (t : ϕ ) → A t)
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
   (is-contr-fiberwise-A : (t : ψ ) → is-contr (A t))
-  : (t : ψ ) → f t = (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t
+  : (t : ψ ) → f t = (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t
   := \ t → eq-is-contr
               ( A t)
               ( is-contr-fiberwise-A t)
               ( f t )
-              ( restrict I ψ ϕ A a (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t)
+              ( restrict I ψ ϕ A a (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t)
 ```
+
 And below proves that `#!rzk c(t) = refl`. Again, this is a consequence of a
 slightly more general statement.
 

From 7f209039e0f2e381ed360f601850f72de83268db Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Mon, 2 Oct 2023 09:09:27 +0200
Subject: [PATCH 16/16] improve naming

---
 src/hott/06-contractible.rzk.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md
index 1d5e0ecf..04aa5c54 100644
--- a/src/hott/06-contractible.rzk.md
+++ b/src/hott/06-contractible.rzk.md
@@ -415,7 +415,7 @@ separate hypothesis.
 Function extensionality implies weak function extensionality.
 
 ```rzk
-#def map-for-weakfunext
+#def map-weakfunext
   (A : U)
   (C : A → U)
   (is-contr-C : (a : A) → is-contr (C a))
@@ -428,12 +428,12 @@ Function extensionality implies weak function extensionality.
   : WeakFunExt
   :=
   \ A C is-contr-C →
-  ( map-for-weakfunext A C is-contr-C ,
+  ( map-weakfunext A C is-contr-C ,
     ( \ g →
       ( eq-htpy funext
         ( A)
         ( C)
-        ( map-for-weakfunext A C is-contr-C)
+        ( map-weakfunext A C is-contr-C)
         ( g)
         ( \ a → second (is-contr-C a) (g a)))))
 ```