Merge branch 'main' into discrete-types-alternative

src/hott/03-equivalences.rzk.md

@@ -535,8 +535,8 @@ The retraction associated with an equivalence is an equivalence.
 
 ## Section-retraction pairs
 
-A pair of maps `s : A' → B` and `r : B → A` is a section-retraction pair if the
-composite `A' → A` is an equivalence.
+A pair of maps `s : A' → B` and `r : B → A` is a **section-retraction pair** if
+the composite `A' → A` is an equivalence.
 
 ```rzk
 #section is-section-retraction-pair

src/hott/08-families-of-maps.rzk.md

@@ -318,35 +318,35 @@ The canonical map from a type to its the free path type is an equivalence.
 #def free-paths
   ( A : U)
   : U
-  := Σ ( (x, y) : product A A) , (x = y)
+  := Σ ( (x , y) : product A A) , (x = y)
 
 #def constant-free-path
   ( A : U)
   ( a : A)
   : free-paths A
-  := ((a,a), refl)
+  := ((a , a) , refl)
 
 #def is-constant-free-path
   ( A : U)
-  ( ((a,y), p) : free-paths A)
+  ( ((a , y) , p) : free-paths A)
   : constant-free-path A a = ((a,y), p)
   :=
     ind-path A a
-    ( \ x p' →  constant-free-path A a = ((a,x), p'))
+    ( \ x p' →  constant-free-path A a = ((a , x) , p'))
     ( refl)
     ( y) ( p)
 
 #def start-free-path
   ( A : U)
   : free-paths A → A
-  := \ ((a,_), _) → a
+  := \ ((a , _) , _) → a
 
 #def is-equiv-constant-free-path
   ( A : U)
   : is-equiv A (free-paths A) (constant-free-path A)
   :=
-    ( ( start-free-path A, \ _ → refl)
-    , ( start-free-path A, is-constant-free-path A))
+    ( ( start-free-path A , \ _ → refl)
+    , ( start-free-path A , is-constant-free-path A))
 ```
 
 ## Pullback of a type family

src/simplicial-hott/05-segal-types.rzk.md

@@ -238,20 +238,20 @@ type.
 
 #def fibered-arr-free-arr
   ( A : U)
-  : (arr A) → (fibered-arr A)
+  : arr A → fibered-arr A
   := \ k → (k 0₂ , (k 1₂ , k))
 
 #def is-equiv-fibered-arr-free-arr
   ( A : U)
   : is-equiv (arr A) (fibered-arr A) (fibered-arr-free-arr A)
   :=
-    ( ( \ (_ , (_ , f)) → f , \ _ → refl)
-    , ( \ (_ , (_ , f)) → f , \ _ → refl))
+    ( ( (\ (_ , (_ , f)) → f) , (\ _ → refl))
+    , ( (\ (_ , (_ , f)) → f) , (\ _ → refl)))
 
 #def equiv-fibered-arr-free-arr
   ( A : U)
   : Equiv (arr A) (fibered-arr A)
-  := ( fibered-arr-free-arr A , is-equiv-fibered-arr-free-arr A)
+  := (fibered-arr-free-arr A , is-equiv-fibered-arr-free-arr A)
 ```
 
 And the corresponding uncurried version.
@@ -266,14 +266,14 @@ And the corresponding uncurried version.
 #def fibered-arr-free-arr'
   ( A : U)
   : arr A → fibered-arr' A
-  := \ σ → ((σ 0₂, σ 1₂), σ)
+  := \ σ → ((σ 0₂ , σ 1₂) , σ)
 
 #def is-equiv-fibered-arr-free-arr'
   ( A : U)
   : is-equiv (arr A) (fibered-arr' A) (fibered-arr-free-arr' A)
   :=
-    ( ( \ ((_ , _) , σ) → σ , \ _ → refl)
-    , ( \ ((_ , _) , σ) → σ , \ _ → refl))
+    ( ( (\ ((_ , _) , σ) → σ) , (\ _ → refl))
+    , ( (\ ((_ , _) , σ) → σ) , (\ _ → refl)))
 ```
 
 ## The Segal condition