From 95afdb88b954a0fd3d45dd43024d78f5f6fded4e Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Mon, 23 Sep 2024 10:05:29 +0200
Subject: [PATCH 1/5] RS17, Proposition 9.10

---
 src/simplicial-hott/09-yoneda.rzk.md | 212 +++++++++++++++++++++++++++
 1 file changed, 212 insertions(+)

diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index fc6d1086..f1796b8e 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -892,6 +892,27 @@ types are contractible.
   := (x : A) → is-contr (hom A a x)
 ```
 
+Initial objects map to initial objects by equivalences.
+
+```rzk
+#def is-inital-equiv-is-initial uses (extext)
+  (A B : U)
+  (e : Equiv A B)
+  (a : A)
+  (is-initial-a : is-initial A a) :
+  is-initial B (first e a)
+  :=
+  \ b →
+    ind-has-section-equiv A B e
+      ( \ b → is-contr (hom B (first e a) b))
+      ( \ a' → is-contr-equiv-is-contr (hom A a a')
+          ( hom B (first e a) (first e a'))
+          ( ap-hom A B (first e) a a'
+          , is-equiv-ap-hom-is-equiv extext A B (first e) (second e) a a')
+      ( is-initial-a a'))
+      ( b)
+```
+
 Initial objects satisfy an induction principle relative to covariant families.
 
 ```rzk
@@ -1114,6 +1135,27 @@ types are contractible.
   := (x : A) → is-contr (hom A x a)
 ```
 
+Final objects map to final objects by equivalences.
+
+```rzk
+#def is-final-equiv-is-final uses (extext)
+  (A B : U)
+  (e : Equiv A B)
+  (a : A)
+  (is-final-a : is-final A a) :
+  is-final B (first e a)
+  :=
+  \ b →
+    ind-has-section-equiv A B e
+      ( \ b → is-contr (hom B b (first e a)))
+      ( \ a' → is-contr-equiv-is-contr (hom A a' a)
+          ( hom B (first e a') (first e a))
+          ( ap-hom A B (first e) a' a
+          , is-equiv-ap-hom-is-equiv extext A B (first e) (second e) a' a)
+      ( is-final-a a'))
+      ( b)
+```
+
 Final objects satisfy an induction principle relative to contravariant families.
 
 ```rzk
@@ -1364,4 +1406,174 @@ condition a name.
   : U
   := Σ ((a , u) : Σ (x : A) , (C x))
       , is-initial (Σ (x : A) , (C x)) (a , u)
+
+#def has-initial-tot-is-representable-family-is-segal uses (extext)
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( C : A → U)
+  ( is-rep-C : is-representable-family A C)
+  : has-initial-tot A C
+  :=
+    ( ( first is-rep-C
+      , evid
+          ( A)
+          ( first is-rep-C)
+          ( C)
+          (equiv-for-is-representable-family A C is-rep-C))
+    , is-inital-equiv-is-initial
+        ( coslice A (first is-rep-C))
+        ( Σ (x : A) , (C x))
+        ( total-equiv-family-of-equiv
+          ( A)
+          (\ x → hom A (first is-rep-C) x)
+          ( C)
+          ( second is-rep-C))
+        ( (first is-rep-C, id-hom A (first is-rep-C)))
+        ( is-initial-id-hom-is-segal A is-segal-A (first is-rep-C)))
+
+#def is-representable-family-has-initial-tot
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( C : A → U)
+  ( is-covariant-C : is-covariant A C)
+  ( has-initial-tot-A : has-initial-tot A C)
+  : (is-representable-family A C)
+  :=
+    ( first(first has-initial-tot-A)
+    , \ b →
+      ( ( yon
+          ( A)
+          ( is-segal-A)
+          ( first(first has-initial-tot-A))
+          ( C)
+          ( is-covariant-C)
+          ( second(first has-initial-tot-A))
+          ( b))
+      , is-equiv-is-contr-map
+        ( hom A ( first(first has-initial-tot-A)) b)
+        ( C b)
+        ( yon
+          ( A)
+          ( is-segal-A)
+          ( first(first has-initial-tot-A))
+          ( C)
+          ( is-covariant-C)
+          ( second(first has-initial-tot-A))
+          ( b))
+        ( \ v →
+          is-contr-equiv-is-contr
+            ( hom (Σ (a : A) , (C a)) (first has-initial-tot-A) (b, v))
+            ( fib
+                ( hom A ( first(first has-initial-tot-A)) b)
+                ( C b)
+                ( yon
+                  ( A)
+                  ( is-segal-A)
+                  ( first(first has-initial-tot-A))
+                  ( C)
+                  ( is-covariant-C)
+                  ( second(first has-initial-tot-A))
+                  ( b))
+                ( v))
+            ( equiv-comp
+              ( hom (Σ (a : A) , (C a)) (first has-initial-tot-A) (b, v))
+              ( Σ (f : hom A (first(first has-initial-tot-A)) b)
+                , dhom
+                  ( A)
+                  ( first(first has-initial-tot-A))
+                  ( b)
+                  ( f)
+                  ( C)
+                  ( second(first has-initial-tot-A))
+                  ( v))
+              ( fib
+                ( hom A (first(first has-initial-tot-A)) b)
+                ( C b)
+                ( yon
+                  ( A)
+                  ( is-segal-A)
+                  ( first(first has-initial-tot-A))
+                  ( C)
+                  ( is-covariant-C)
+                  ( second(first has-initial-tot-A))
+                  ( b))
+                ( v))
+              ( axiom-choice
+                    ( 2)
+                    ( Δ¹)
+                    ( ∂Δ¹)
+                    ( \ _ → A)
+                    ( \ t x → C x)
+                    ( \ t →
+                      recOR
+                        ( t ≡ 0₂ ↦ first(first has-initial-tot-A)
+                        , t ≡ 1₂ ↦ b))
+                    ( \ t →
+                      recOR
+                        ( t ≡ 0₂ ↦ second(first has-initial-tot-A)
+                        , t ≡ 1₂ ↦ v)))
+              ( total-equiv-family-of-equiv
+                ( hom A (first(first has-initial-tot-A)) b)
+                ( \ f →
+                  dhom
+                    ( A)
+                    ( first(first has-initial-tot-A))
+                    ( b)
+                    ( f)
+                    ( C)
+                    ( second(first has-initial-tot-A))
+                    ( v))
+                ( \ f →
+                  covariant-transport
+                    ( A)
+                    ( first(first has-initial-tot-A))
+                    ( b)
+                    ( f)
+                    ( C)
+                    ( is-covariant-C)
+                    ( second(first has-initial-tot-A))
+                  = v)
+                ( \ f →
+                    ( covariant-uniqueness-curried
+                      ( A)
+                      ( first(first has-initial-tot-A))
+                      ( b)
+                      ( f)
+                      ( C)
+                      ( is-covariant-C)
+                      ( second(first has-initial-tot-A))
+                      ( v)
+                    , is-equiv-covariant-uniqueness-curried
+                      ( A)
+                      ( first(first has-initial-tot-A))
+                      ( b)
+                      ( f)
+                      ( C)
+                      ( is-covariant-C)
+                      ( second(first has-initial-tot-A))
+                      ( v)))))
+            ( second has-initial-tot-A (b, v)))))
+```
+
+```rzk title="RS17, Proposition 9.10"
+#def is-representable-iff-has-initial-tot uses (extext)
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( C : A → U)
+  ( is-covariant-C : is-covariant A C)
+  : iff (is-representable-family A C) (has-initial-tot A C)
+  :=
+    ( \ is-rep-C →
+      has-initial-tot-is-representable-family-is-segal
+      ( A)
+      ( is-segal-A)
+      ( C)
+      ( is-rep-C)
+    , \ has-initial-tot-A →
+      is-representable-family-has-initial-tot
+      ( A)
+      ( is-segal-A)
+      ( C)
+      ( is-covariant-C)
+      ( has-initial-tot-A))
 ```

From 7a7758b2479cc182247517e51f985ad0e6fdde63 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Sun, 29 Sep 2024 16:01:48 +0200
Subject: [PATCH 2/5] Formatting

---
 src/simplicial-hott/09-yoneda.rzk.md | 41 +++++++++++++++-------------
 1 file changed, 22 insertions(+), 19 deletions(-)

diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index f1796b8e..ec1c682b 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -896,10 +896,11 @@ Initial objects map to initial objects by equivalences.
 
 ```rzk
 #def is-inital-equiv-is-initial uses (extext)
-  (A B : U)
-  (e : Equiv A B)
-  (a : A)
-  (is-initial-a : is-initial A a) :
+  ( A B : U)
+  ( e : Equiv A B)
+  ( a : A)
+  ( is-initial-a : is-initial A a)
+  :
   is-initial B (first e a)
   :=
   \ b →
@@ -1139,10 +1140,11 @@ Final objects map to final objects by equivalences.
 
 ```rzk
 #def is-final-equiv-is-final uses (extext)
-  (A B : U)
-  (e : Equiv A B)
-  (a : A)
-  (is-final-a : is-final A a) :
+  ( A B : U)
+  ( e : Equiv A B)
+  ( a : A)
+  ( is-final-a : is-final A a)
+  :
   is-final B (first e a)
   :=
   \ b →
@@ -1419,16 +1421,16 @@ condition a name.
           ( A)
           ( first is-rep-C)
           ( C)
-          (equiv-for-is-representable-family A C is-rep-C))
+          ( equiv-for-is-representable-family A C is-rep-C))
     , is-inital-equiv-is-initial
         ( coslice A (first is-rep-C))
-        ( Σ (x : A) , (C x))
+        ( Σ ( x : A) , (C x))
         ( total-equiv-family-of-equiv
           ( A)
-          (\ x → hom A (first is-rep-C) x)
+          ( \ x → hom A (first is-rep-C) x)
           ( C)
           ( second is-rep-C))
-        ( (first is-rep-C, id-hom A (first is-rep-C)))
+        ( ( first is-rep-C , id-hom A (first is-rep-C)))
         ( is-initial-id-hom-is-segal A is-segal-A (first is-rep-C)))
 
 #def is-representable-family-has-initial-tot
@@ -1437,7 +1439,7 @@ condition a name.
   ( C : A → U)
   ( is-covariant-C : is-covariant A C)
   ( has-initial-tot-A : has-initial-tot A C)
-  : (is-representable-family A C)
+  : ( is-representable-family A C)
   :=
     ( first(first has-initial-tot-A)
     , \ b →
@@ -1450,7 +1452,7 @@ condition a name.
           ( second(first has-initial-tot-A))
           ( b))
       , is-equiv-is-contr-map
-        ( hom A ( first(first has-initial-tot-A)) b)
+        ( hom A (first(first has-initial-tot-A)) b)
         ( C b)
         ( yon
           ( A)
@@ -1462,9 +1464,9 @@ condition a name.
           ( b))
         ( \ v →
           is-contr-equiv-is-contr
-            ( hom (Σ (a : A) , (C a)) (first has-initial-tot-A) (b, v))
+            ( hom (Σ (a : A) , (C a)) (first has-initial-tot-A) (b , v))
             ( fib
-                ( hom A ( first(first has-initial-tot-A)) b)
+                ( hom A (first(first has-initial-tot-A)) b)
                 ( C b)
                 ( yon
                   ( A)
@@ -1476,8 +1478,8 @@ condition a name.
                   ( b))
                 ( v))
             ( equiv-comp
-              ( hom (Σ (a : A) , (C a)) (first has-initial-tot-A) (b, v))
-              ( Σ (f : hom A (first(first has-initial-tot-A)) b)
+              ( hom (Σ (a : A) , (C a)) (first has-initial-tot-A) (b , v))
+              ( Σ ( f : hom A (first(first has-initial-tot-A)) b)
                 , dhom
                   ( A)
                   ( first(first has-initial-tot-A))
@@ -1552,7 +1554,7 @@ condition a name.
                       ( is-covariant-C)
                       ( second(first has-initial-tot-A))
                       ( v)))))
-            ( second has-initial-tot-A (b, v)))))
+            ( second has-initial-tot-A (b , v)))))
 ```
 
 ```rzk title="RS17, Proposition 9.10"
@@ -1577,3 +1579,4 @@ condition a name.
       ( is-covariant-C)
       ( has-initial-tot-A))
 ```
+

From 64159808b076415b3f205086d31f6fc77af4623b Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Mon, 30 Sep 2024 21:41:09 +0200
Subject: [PATCH 3/5] Code explanation

---
 src/simplicial-hott/09-yoneda.rzk.md | 51 +++++++++++++++++++---------
 1 file changed, 35 insertions(+), 16 deletions(-)

diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index ec1c682b..23e63870 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -1408,7 +1408,13 @@ condition a name.
   : U
   := Σ ((a , u) : Σ (x : A) , (C x))
       , is-initial (Σ (x : A) , (C x)) (a , u)
+```
+
+As a representable family is fiberwise equivalent to a `#!rzk Σ (x : A) , C x`,
+the total space of the family is equivalent to a coslice, and coslices have an
+initial object by `#!rzk is-initial-id-hom-is-segal`.
 
+```rzk
 #def has-initial-tot-is-representable-family-is-segal uses (extext)
   ( A : U)
   ( is-segal-A : is-segal A)
@@ -1433,6 +1439,19 @@ condition a name.
         ( ( first is-rep-C , id-hom A (first is-rep-C)))
         ( is-initial-id-hom-is-segal A is-segal-A (first is-rep-C)))
 
+```
+
+The other direction is a bit longer. We follow the proof of RS17 9.10:
+given `#!rzk (a, u) : Σ (x : A) , C x` an initial object of
+`#!rzk Σ (x : A) , C x`, evaluating `#!rzk yon` at `#!rzk u : C a`
+yields a family of maps `#!rzk (x : A) → hom A a x → C x`. This is a
+contractible map as its fiber at `#!rzk (b : A, v : C b)` is equivalent
+to the hom type `#!rzk hom (Σ (x : A) , C x) (a, u) (b, v)` through
+the composite of `#!rzk covariant-uniqueness-curried` and
+`#!rzk axiom-choice` and it is thus an equivalence using
+`#!rzk is-equiv-is-contr-map`.
+
+```rzk
 #def is-representable-family-has-initial-tot
   ( A : U)
   ( is-segal-A : is-segal A)
@@ -1441,23 +1460,23 @@ condition a name.
   ( has-initial-tot-A : has-initial-tot A C)
   : ( is-representable-family A C)
   :=
-    ( first(first has-initial-tot-A)
+    ( first (first has-initial-tot-A)
     , \ b →
       ( ( yon
           ( A)
           ( is-segal-A)
-          ( first(first has-initial-tot-A))
+          ( first (first has-initial-tot-A))
           ( C)
           ( is-covariant-C)
           ( second(first has-initial-tot-A))
           ( b))
       , is-equiv-is-contr-map
-        ( hom A (first(first has-initial-tot-A)) b)
+        ( hom A (first (first has-initial-tot-A)) b)
         ( C b)
         ( yon
           ( A)
           ( is-segal-A)
-          ( first(first has-initial-tot-A))
+          ( first (first has-initial-tot-A))
           ( C)
           ( is-covariant-C)
           ( second(first has-initial-tot-A))
@@ -1466,12 +1485,12 @@ condition a name.
           is-contr-equiv-is-contr
             ( hom (Σ (a : A) , (C a)) (first has-initial-tot-A) (b , v))
             ( fib
-                ( hom A (first(first has-initial-tot-A)) b)
+                ( hom A (first (first has-initial-tot-A)) b)
                 ( C b)
                 ( yon
                   ( A)
                   ( is-segal-A)
-                  ( first(first has-initial-tot-A))
+                  ( first (first has-initial-tot-A))
                   ( C)
                   ( is-covariant-C)
                   ( second(first has-initial-tot-A))
@@ -1479,22 +1498,22 @@ condition a name.
                 ( v))
             ( equiv-comp
               ( hom (Σ (a : A) , (C a)) (first has-initial-tot-A) (b , v))
-              ( Σ ( f : hom A (first(first has-initial-tot-A)) b)
+              ( Σ ( f : hom A (first (first has-initial-tot-A)) b)
                 , dhom
                   ( A)
-                  ( first(first has-initial-tot-A))
+                  ( first (first has-initial-tot-A))
                   ( b)
                   ( f)
                   ( C)
                   ( second(first has-initial-tot-A))
                   ( v))
               ( fib
-                ( hom A (first(first has-initial-tot-A)) b)
+                ( hom A (first (first has-initial-tot-A)) b)
                 ( C b)
                 ( yon
                   ( A)
                   ( is-segal-A)
-                  ( first(first has-initial-tot-A))
+                  ( first (first has-initial-tot-A))
                   ( C)
                   ( is-covariant-C)
                   ( second(first has-initial-tot-A))
@@ -1508,18 +1527,18 @@ condition a name.
                     ( \ t x → C x)
                     ( \ t →
                       recOR
-                        ( t ≡ 0₂ ↦ first(first has-initial-tot-A)
+                        ( t ≡ 0₂ ↦ first (first has-initial-tot-A)
                         , t ≡ 1₂ ↦ b))
                     ( \ t →
                       recOR
                         ( t ≡ 0₂ ↦ second(first has-initial-tot-A)
                         , t ≡ 1₂ ↦ v)))
               ( total-equiv-family-of-equiv
-                ( hom A (first(first has-initial-tot-A)) b)
+                ( hom A (first (first has-initial-tot-A)) b)
                 ( \ f →
                   dhom
                     ( A)
-                    ( first(first has-initial-tot-A))
+                    ( first (first has-initial-tot-A))
                     ( b)
                     ( f)
                     ( C)
@@ -1528,7 +1547,7 @@ condition a name.
                 ( \ f →
                   covariant-transport
                     ( A)
-                    ( first(first has-initial-tot-A))
+                    ( first (first has-initial-tot-A))
                     ( b)
                     ( f)
                     ( C)
@@ -1538,7 +1557,7 @@ condition a name.
                 ( \ f →
                     ( covariant-uniqueness-curried
                       ( A)
-                      ( first(first has-initial-tot-A))
+                      ( first (first has-initial-tot-A))
                       ( b)
                       ( f)
                       ( C)
@@ -1547,7 +1566,7 @@ condition a name.
                       ( v)
                     , is-equiv-covariant-uniqueness-curried
                       ( A)
-                      ( first(first has-initial-tot-A))
+                      ( first (first has-initial-tot-A))
                       ( b)
                       ( f)
                       ( C)

From b10c90a589f27eb5de2c8ee06bc659be63daa7f2 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Mon, 30 Sep 2024 21:43:16 +0200
Subject: [PATCH 4/5] Prettier

---
 src/simplicial-hott/09-yoneda.rzk.md | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index 23e63870..50e0e68c 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -1441,15 +1441,14 @@ initial object by `#!rzk is-initial-id-hom-is-segal`.
 
 ```
 
-The other direction is a bit longer. We follow the proof of RS17 9.10:
-given `#!rzk (a, u) : Σ (x : A) , C x` an initial object of
-`#!rzk Σ (x : A) , C x`, evaluating `#!rzk yon` at `#!rzk u : C a`
-yields a family of maps `#!rzk (x : A) → hom A a x → C x`. This is a
-contractible map as its fiber at `#!rzk (b : A, v : C b)` is equivalent
-to the hom type `#!rzk hom (Σ (x : A) , C x) (a, u) (b, v)` through
-the composite of `#!rzk covariant-uniqueness-curried` and
-`#!rzk axiom-choice` and it is thus an equivalence using
-`#!rzk is-equiv-is-contr-map`.
+The other direction is a bit longer. We follow the proof of RS17 9.10: given
+`#!rzk (a, u) : Σ (x : A) , C x` an initial object of `#!rzk Σ (x : A) , C x`,
+evaluating `#!rzk yon` at `#!rzk u : C a` yields a family of maps
+`#!rzk (x : A) → hom A a x → C x`. This is a contractible map as its fiber at
+`#!rzk (b : A, v : C b)` is equivalent to the hom type
+`#!rzk hom (Σ (x : A) , C x) (a, u) (b, v)` through the composite of
+`#!rzk covariant-uniqueness-curried` and `#!rzk axiom-choice` and it is thus an
+equivalence using `#!rzk is-equiv-is-contr-map`.
 
 ```rzk
 #def is-representable-family-has-initial-tot
@@ -1598,4 +1597,3 @@ the composite of `#!rzk covariant-uniqueness-curried` and
       ( is-covariant-C)
       ( has-initial-tot-A))
 ```
-

From 8996f347bca29dad60d60dbc11231817fb390200 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Tue, 1 Oct 2024 09:27:23 +0200
Subject: [PATCH 5/5] Formatting, name

---
 src/simplicial-hott/09-yoneda.rzk.md | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index 50e0e68c..a5fa2089 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -1415,7 +1415,7 @@ the total space of the family is equivalent to a coslice, and coslices have an
 initial object by `#!rzk is-initial-id-hom-is-segal`.
 
 ```rzk
-#def has-initial-tot-is-representable-family-is-segal uses (extext)
+#def has-initial-tot-is-representable-family uses (extext)
   ( A : U)
   ( is-segal-A : is-segal A)
   ( C : A → U)
@@ -1467,7 +1467,7 @@ equivalence using `#!rzk is-equiv-is-contr-map`.
           ( first (first has-initial-tot-A))
           ( C)
           ( is-covariant-C)
-          ( second(first has-initial-tot-A))
+          ( second (first has-initial-tot-A))
           ( b))
       , is-equiv-is-contr-map
         ( hom A (first (first has-initial-tot-A)) b)
@@ -1478,7 +1478,7 @@ equivalence using `#!rzk is-equiv-is-contr-map`.
           ( first (first has-initial-tot-A))
           ( C)
           ( is-covariant-C)
-          ( second(first has-initial-tot-A))
+          ( second (first has-initial-tot-A))
           ( b))
         ( \ v →
           is-contr-equiv-is-contr
@@ -1492,7 +1492,7 @@ equivalence using `#!rzk is-equiv-is-contr-map`.
                   ( first (first has-initial-tot-A))
                   ( C)
                   ( is-covariant-C)
-                  ( second(first has-initial-tot-A))
+                  ( second (first has-initial-tot-A))
                   ( b))
                 ( v))
             ( equiv-comp
@@ -1504,7 +1504,7 @@ equivalence using `#!rzk is-equiv-is-contr-map`.
                   ( b)
                   ( f)
                   ( C)
-                  ( second(first has-initial-tot-A))
+                  ( second (first has-initial-tot-A))
                   ( v))
               ( fib
                 ( hom A (first (first has-initial-tot-A)) b)
@@ -1515,7 +1515,7 @@ equivalence using `#!rzk is-equiv-is-contr-map`.
                   ( first (first has-initial-tot-A))
                   ( C)
                   ( is-covariant-C)
-                  ( second(first has-initial-tot-A))
+                  ( second (first has-initial-tot-A))
                   ( b))
                 ( v))
               ( axiom-choice
@@ -1530,7 +1530,7 @@ equivalence using `#!rzk is-equiv-is-contr-map`.
                         , t ≡ 1₂ ↦ b))
                     ( \ t →
                       recOR
-                        ( t ≡ 0₂ ↦ second(first has-initial-tot-A)
+                        ( t ≡ 0₂ ↦ second (first has-initial-tot-A)
                         , t ≡ 1₂ ↦ v)))
               ( total-equiv-family-of-equiv
                 ( hom A (first (first has-initial-tot-A)) b)
@@ -1541,7 +1541,7 @@ equivalence using `#!rzk is-equiv-is-contr-map`.
                     ( b)
                     ( f)
                     ( C)
-                    ( second(first has-initial-tot-A))
+                    ( second (first has-initial-tot-A))
                     ( v))
                 ( \ f →
                   covariant-transport
@@ -1551,7 +1551,7 @@ equivalence using `#!rzk is-equiv-is-contr-map`.
                     ( f)
                     ( C)
                     ( is-covariant-C)
-                    ( second(first has-initial-tot-A))
+                    ( second (first has-initial-tot-A))
                   = v)
                 ( \ f →
                     ( covariant-uniqueness-curried
@@ -1561,7 +1561,7 @@ equivalence using `#!rzk is-equiv-is-contr-map`.
                       ( f)
                       ( C)
                       ( is-covariant-C)
-                      ( second(first has-initial-tot-A))
+                      ( second (first has-initial-tot-A))
                       ( v)
                     , is-equiv-covariant-uniqueness-curried
                       ( A)
@@ -1570,7 +1570,7 @@ equivalence using `#!rzk is-equiv-is-contr-map`.
                       ( f)
                       ( C)
                       ( is-covariant-C)
-                      ( second(first has-initial-tot-A))
+                      ( second (first has-initial-tot-A))
                       ( v)))))
             ( second has-initial-tot-A (b , v)))))
 ```
@@ -1584,7 +1584,7 @@ equivalence using `#!rzk is-equiv-is-contr-map`.
   : iff (is-representable-family A C) (has-initial-tot A C)
   :=
     ( \ is-rep-C →
-      has-initial-tot-is-representable-family-is-segal
+      has-initial-tot-is-representable-family
       ( A)
       ( is-segal-A)
       ( C)