Clean up Chapter 2 a bit

src/1-foundations/2-homotopy-type-theory/04-homotopies-and-equivalences.rzk.md

@@ -375,12 +375,21 @@ which are discussed in Sections [2.6](06-cartesian-product-types.rzk.md) and [2.
 ### Symmetry
 
 ```rzk
+#def inverse-from-isequiv
+  ( A B : U)
+  ( f : A → B)
+  : isequiv A B f → (B → A)
+  :=
+  \ isequiv-f →
+    inverse-from-qinv A B f
+    ( isequiv-to-qinv A B f isequiv-f)
+
 #def inverse-from-equivalence
   ( A B : U)
   : equivalence A B → (B → A)
   :=
   \ (f , isequiv-f) →
-    inverse-from-qinv A B f (isequiv-to-qinv A B f isequiv-f)
+    inverse-from-isequiv A B f isequiv-f
 
 #def isequiv-inverse-from-equivalence
   ( A B : U)

src/1-foundations/2-homotopy-type-theory/06-cartesian-product-types.rzk.md

@@ -12,12 +12,19 @@ For any elements $x, y : A \times B$ and a path $p : x =_{A \times B} y$, by fun
 #def path-in-prod-to-prod-of-paths
   ( A B : U)
   ( x y : prod A B)
-  : ( x = y) → prod (pr₁ A B x = pr₁ A B y) (pr₂ A B x = pr₂ A B y)
-  := \ p → (ap (prod A B) A (pr₁ A B) x y p , ap (prod A B) B (pr₂ A B) x y p)
+  : ( x = y)
+  → prod
+    ( pr₁ A B x = pr₁ A B y)
+    ( pr₂ A B x = pr₂ A B y)
+  :=
+  \ p →
+    ( ap (prod A B) A (pr₁ A B) x y p
+    , ap (prod A B) B (pr₂ A B) x y p)
 ```
 
 
 !!! note "Theorem 2.6.2. Paths in a product space are pairs of paths"
+
     The function
 
     $$(x =_{A \times B} y) → (\mathsf{pr}_1(x) =_A \mathsf{pr}_1(y)) \times (\mathsf{pr}_2(x) =_B \mathsf{pr}_2(y)).$$
@@ -29,15 +36,22 @@ For any elements $x, y : A \times B$ and a path $p : x =_{A \times B} y$, by fun
   ( A B : U)
   ( a₁ a₂ : A)
   ( b₁ b₂ : B)
-  : ( prod (a₁ = a₂) (b₁ = b₂)) → (a₁ , b₁) = (a₂ , b₂)
-  := \ (pa , pb) → path-ind A
-      ( \ x y p → (x , b₁) = (y , b₂))
-      ( \ x → path-ind B
-        ( \ x' y' p' → (x , x') = (x , y'))
-        ( \ x' → refl)
-        b₁ b₂ pb
-      )
-      a₁ a₂ pa
+  : prod (a₁ = a₂) (b₁ = b₂)
+  → ( a₁ , b₁) = (a₂ , b₂)
+  :=
+  \ (pa , pb) →
+    path-ind A
+    ( \ x y p → (x , b₁) = (y , b₂))
+    ( \ x →
+        path-ind B
+        ( \ x' y' _p' → (x , x') = (x , y'))
+        ( \ _x' → refl)
+        ( b₁)
+        ( b₂)
+        ( pb))
+    ( a₁)
+    ( a₂)
+    ( pa)
 ```
 
 
@@ -46,20 +60,45 @@ For any elements $x, y : A \times B$ and a path $p : x =_{A \times B} y$, by fun
   ( A B : U)
   ( a₁ a₂ : A)
   ( b₁ b₂ : B)
-  : qinv ((a₁ , b₁) = (a₂ , b₂)) (prod (a₁ = a₂) (b₁ = b₂)) (path-in-prod-to-prod-of-paths A B (a₁ , b₁) (a₂ , b₂))
-  := (prod-of-paths-to-path-in-prod A B a₁ a₂ b₁ b₂
-    , ( \ (pa , pb) → path-ind A
-          ( \ x y p → (path-in-prod-to-prod-of-paths A B (x , b₁) (y , b₂)) (prod-of-paths-to-path-in-prod A B x y b₁ b₂ (p , pb)) = (p , pb))
-          ( \ x → path-ind B
-              ( \ x' y' p' → ((path-in-prod-to-prod-of-paths A B (x , x') (x , y')) (prod-of-paths-to-path-in-prod A B x x x' y' (refl , p')) = (refl , p')))
-              ( \ x' → refl)
-              b₁ b₂ pb
-          )
-          a₁ a₂ pa
-      , \ pab → path-ind (prod A B)
-          ( \ (a₁' , b₁') (a₂' , b₂') pab' → prod-of-paths-to-path-in-prod A B a₁' a₂' b₁' b₂' (path-in-prod-to-prod-of-paths A B (a₁' , b₁') (a₂' , b₂') pab') = pab')
+  : qinv
+    ( ( a₁ , b₁) = (a₂ , b₂))
+    ( prod (a₁ = a₂) (b₁ = b₂))
+    ( path-in-prod-to-prod-of-paths A B (a₁ , b₁) (a₂ , b₂))
+  :=
+  ( prod-of-paths-to-path-in-prod A B a₁ a₂ b₁ b₂
+  , ( \ (pa , pb) →
+        path-ind A
+        ( \ x y p →
+          path-in-prod-to-prod-of-paths A B (x , b₁) (y , b₂)
+          ( prod-of-paths-to-path-in-prod A B x y b₁ b₂
+            ( p , pb))
+        = ( p , pb))
+        ( \ x →
+            path-ind B
+            ( \ x' y' p' →
+                path-in-prod-to-prod-of-paths A B (x , x') (x , y')
+                ( prod-of-paths-to-path-in-prod A B x x x' y'
+                  ( refl , p'))
+              = ( refl , p'))
+            ( \ x' → refl)
+            ( b₁)
+            ( b₂)
+            ( pb)
+        )
+        ( a₁)
+        ( a₂)
+        ( pa)
+      , \ pab →
+          path-ind (prod A B)
+          ( \ (a₁' , b₁') (a₂' , b₂') pab' →
+              prod-of-paths-to-path-in-prod A B a₁' a₂' b₁' b₂'
+              ( path-in-prod-to-prod-of-paths A B (a₁' , b₁') (a₂' , b₂')
+                ( pab'))
+            = pab')
           ( \ x → refl)
-          ( a₁ , b₁) (a₂ , b₂) pab
+          ( a₁ , b₁)
+          ( a₂ , b₂)
+          ( pab)
       )
   )
 ```

src/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk.md

@@ -5,30 +5,29 @@ This is a literate Rzk file:
 ```rzk
 #lang rzk-1
 ```
-For `Unit` type, uniqueness principle is built-in. That is, for any `x, y : Unit`, we have `refl : x = y`
+
+For `#!rzk Unit` type, uniqueness principle is built-in. That is, for any `#!rzk x, y : Unit`, we have `#!rzk refl : x = y`
 
 !!! note "Theorem 2.8.1."
-    For any $x,y:\mathbb{1}$, we have $(x=y) \simeq \mathbb{1}$.
+
+    For any $x, y : \mathbb{1}$, we have $(x = y) \simeq \mathbb{1}$.
 
 ```rzk
 #def paths-in-unit-equiv-unit
     ( x y : Unit)
   : equivalence (x = y) Unit
     -- provide a function - a constant map to unit
-  := (\ (p : x = y) → unit , (
-        -- provide right inverse - a constant map to refl_{unit}
-        ( \ (u : Unit) → refl_{unit}
+  :=
+  ( \ (p : x = y) → unit
+  , ( -- provide right inverse - a constant map to refl_{unit}
+      ( \ (u : Unit) → refl_{unit}
       , -- prove that composition is homotopical to id_Unit
-            \ (u : Unit) → refl)
-      , -- provide left inverse - a constant map to refl_{unit}
-        ( \ (u : Unit) → refl_{unit}
+        \ (u : Unit) → refl)
+    , -- provide left inverse - a constant map to refl_{unit}
+      ( \ (u : Unit) → refl_{unit}
       , -- prove that composition is homotopical to id_{x = y}; use path induction on p
-            \ (p : x = y) → path-ind
-                Unit
-                ( \ x' y' p' → refl_{unit} = p')
-                ( \ x' → refl)
-                x y p
-            )
-        ))
+        path-ind Unit
+        ( \ x' y' p' → refl_{unit} = p')
+        ( \ x' → refl)
+        x y)))
 ```
-

src/1-foundations/2-homotopy-type-theory/09-pi-types-and-function-extensionality.rzk.md

@@ -5,3 +5,43 @@ This is a literate Rzk file:
 ```rzk
 #lang rzk-1
 ```
+
+```rzk title="HoTT Book, Definition 2.9.2"
+#define happly
+  ( A : U)
+  ( B : A → U)
+  ( f g : (a : A) → B a)
+  : ( f = g) → homotopy A B f g
+  :=
+  path-ind ((a : A) → B a)
+  ( \ f' g' _ → homotopy A B f' g')
+  ( \ f' _ → refl)
+  f g
+```
+
+```rzk title="HoTT Book, Axiom 2.9.3"
+#define FunExt
+  : U
+  :=
+    ( A : U)
+  → ( B : A → U)
+  → ( f : (a : A) → B a)
+  → ( g : (a : A) → B a)
+  → isequiv
+    ( f = g)
+    ( homotopy A B f g)
+    ( happly A B f g)
+```
+
+```rzk
+#assume funext : FunExt
+```
+
+```rzk
+#define map-funext uses (funext)
+  ( A : U)
+  ( B : A → U)
+  ( f g : (a : A) → B a)
+  : homotopy A B f g → f = g
+  := first (second (funext A B f g))
+```