cosmetic edits

src/hott/02-homotopies.rzk.md

@@ -145,12 +145,12 @@ $K^{-1} \cdot H  \sim \text{refl-htpy}_{g}$
   : comp A B C h f = comp A B C k g
   :=
     ind-path (A → B) f (\ g' p' → comp A B C h f = comp A B C k g')
-      ( ind-path (B → C) h (\ k' q' → comp A B C h f = comp A B C k' f)
-        ( refl)
-        ( k)
-        ( q))
-      ( g)
-      ( p)
+    ( ind-path (B → C) h (\ k' q' → comp A B C h f = comp A B C k' f)
+      ( refl)
+      ( k)
+      ( q))
+    ( g)
+    ( p)
 ```
 
 ## Naturality

src/hott/03-equivalences.rzk.md

@@ -821,9 +821,9 @@ identifications. This defines `#!rzk eq-htpy` to be the retraction to
   : (comp A B A (π₁ (π₁ is-equiv-f)) f) = (identity A)
   :=
     eq-htpy A (\ x' → A)
-      ( comp A B A (π₁ (π₁ is-equiv-f)) f)
-      ( identity A)
-      ( π₂ (π₁ is-equiv-f))
+    ( comp A B A (π₁ (π₁ is-equiv-f)) f)
+    ( identity A)
+    ( π₂ (π₁ is-equiv-f))
 
 #def right-cancel-is-equiv uses (funext)
   ( A B : U)
@@ -832,9 +832,9 @@ identifications. This defines `#!rzk eq-htpy` to be the retraction to
   : (comp B A B f (π₁ (π₂ is-equiv-f))) = (identity B)
   :=
     eq-htpy B (\ x' → B)
-      ( comp B A B f (π₁ (π₂ is-equiv-f)))
-      ( identity B)
-      ( π₂ (π₂ is-equiv-f))
+    ( comp B A B f (π₁ (π₂ is-equiv-f)))
+    ( identity B)
+    ( π₂ (π₂ is-equiv-f))
 ```
 
 Using function extensionality, a fiberwise equivalence defines an equivalence of

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

@@ -10,10 +10,8 @@ This is a literate `rzk` file:
 
 ## Prerequisites
 
-- `hott/4-equivalences.rzk` — contains the definitions of `#!rzk Equiv` and
+- `hott/03-equivalences.rzk.md` — contains the definitions of `#!rzk Equiv` and
   `#!rzk comp-equiv`
-- the file `hott/4-equivalences.rzk` relies in turn on the previous files in
-  `hott/`
 
 ## Extension up to homotopy
 
@@ -371,10 +369,10 @@ For each of these we provide a corresponding functorial instance
     ( (t : ψ) → (Σ (x : X t) , Y t x) [ϕ t ↦ (a t , b t)])
   :=
     inv-equiv
-      ( (t : ψ) → (Σ (x : X t) , Y t x) [ϕ t ↦ (a t , b t)])
-      ( Σ ( f : ((t : ψ) → X t [ϕ t ↦ a t]))
+    ( (t : ψ) → (Σ (x : X t) , Y t x) [ϕ t ↦ (a t , b t)])
+    ( Σ ( f : ((t : ψ) → X t [ϕ t ↦ a t]))
       , ( (t : ψ) → Y t (f t) [ϕ t ↦ b t]))
-      ( axiom-choice I ψ ϕ X Y a b)
+    ( axiom-choice I ψ ϕ X Y a b)
 ```
 
 ## Composites and unions of cofibrations

src/simplicial-hott/06-2cat-of-segal-types.rzk.md

@@ -10,10 +10,10 @@ This is a literate `rzk` file:
 
 ## Prerequisites
 
-- `3-simplicial-type-theory.md` — We rely on definitions of simplicies and their
-  subshapes.
-- `4-extension-types.md` — We use extension extensionality.
-- `5-segal-types.md` - We use the notion of hom types.
+- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and
+  their subshapes.
+- `03-extension-types.rzk.md` — We use extension extensionality.
+- `05-segal-types.rzk.md` - We use the notion of hom types.
 
 Some of the definitions in this file rely on function extensionality and
 extension extensionality: