Apply suggestions from code review

Co-authored-by: Fredrik Bakke <[email protected]>

src/hott/03-equivalences.rzk.md

@@ -421,8 +421,8 @@ retraction the first map is an equivalence, and dually.
   ( ( ( retr-gf, η-gf), (sec-gf, ε-gf)) : is-equiv A C (comp A B C g f))
   : is-equiv B C g
   :=
-    ( ( comp C A B f retr-gf ,
-        ind-has-section A B f has-section-f
+    ( ( comp C A B f retr-gf
+      , ind-has-section A B f has-section-f
           ( \ b → f (retr-gf (g b)) = b)
           ( \ a → ap A B (retr-gf (g (f a))) a f (η-gf a)))
     , ( comp C A B f sec-gf, ε-gf))

src/simplicial-hott/03-extension-types.rzk.md

@@ -70,8 +70,8 @@ restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of
   : has-section (extension-type σ) (homotopy-extension-type σ)
       (extension-type-weakening-map σ)
   :=
-    ( extension-strictification σ,
-      \ th → ( second (section-extension-type-weakening' σ th)))
+    ( extension-strictification σ
+    , \ th → ( second (section-extension-type-weakening' σ th)))
 
 
 #def is-equiv-extension-type-weakening
@@ -120,9 +120,7 @@ This equivalence is functorial in the following sense:
       , \ _ → refl
       )
     , ( is-equiv-extension-type-weakening I ψ ϕ A' σ'
-      , is-equiv-extension-type-weakening I ψ ϕ A (\ t → α t (σ' t))
-      )
-    )
+      , is-equiv-extension-type-weakening I ψ ϕ A (\ t → α t (σ' t))))
 ```
 
 ## Commutation of arguments and currying
@@ -1095,7 +1093,7 @@ pointwise.
     ( \ τ → (t : ϕ) → (τ t = σ t))
     ( \ τ →
       equiv-ExtExt extext I (\ t → ϕ t) (\ _ → BOT) (\ t → A t)
-      ( \ _ → recBOT) ( \ t → τ t) ( σ))
+      ( \ _ → recBOT) (\ t → τ t) σ)
 
 #def extension-type-pointwise-weakening uses (extext)
   ( σ : (t : ϕ) → A t)
@@ -1132,7 +1130,7 @@ Given a map `α : A' → A`, there is also a notion of relative extension types.
   : U
   :=
     Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t])
-    , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl]
+    , ( ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl])
 
 #def relative-extension-type'
   : U
@@ -1182,24 +1180,24 @@ with a `τ : ψ → A` that does not strictly restrict to `\ t → α (σ' t)`.
     , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ h t]
 ```
 
-If all ordinary relative extension types are contractible, then also all
-generalized ones.
+If all ordinary relative extension types are contractible, then all
+generalized extension types are also contractible.
 
 ```rzk
 #def has-contr-relative-extension-types
   : U
   :=
-    ( σ' : (t : ϕ) → A' t)
+  ( ( σ' : (t : ϕ) → A' t)
   → ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)])
-  → ( is-contr (relative-extension-type I ψ ϕ A' A α σ' τ))
+  → ( is-contr (relative-extension-type I ψ ϕ A' A α σ' τ)))
 
 #def has-contr-general-relative-extension-types
   : U
   :=
-    ( σ' : (t : ϕ) → A' t)
+  ( ( σ' : (t : ϕ) → A' t)
   → ( τ : (t : ψ) → A t)
   → ( h : (t : ϕ) → α t (σ' t) = τ t)
-  → ( is-contr ( general-relative-extension-type σ' τ h))
+  → ( is-contr ( general-relative-extension-type σ' τ h)))
 
 #def has-contr-relative-extension-types-generalize' uses (extext)
   ( has-contr-relext-α : has-contr-relative-extension-types)

src/simplicial-hott/04-right-orthogonal.rzk.md

@@ -90,8 +90,7 @@ extension types.
         ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ)
       ( equiv-relative-extension-type-fib extext I ψ ϕ
         ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ)
-      ( are-contr-relext-α σ' τ)
-    )
+      ( are-contr-relext-α σ' τ))
 
 #def has-contr-relative-extension-types-is-right-orthogonal-to-shape uses (extext)
   ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)