format

src/hott/03-equivalences.rzk.md

@@ -224,9 +224,9 @@ The type of equivalences between types uses `#!rzk is-equiv` rather than
 
 ## Induction with section
 
-We have two variants of induction with section that say that if `f : A → B`
-has a section, it suffices to prove statements about `b : B` by doing so terms
-of the form `f a`.
+We have two variants of induction with section that say that if `f : A → B` has
+a section, it suffices to prove statements about `b : B` by doing so terms of
+the form `f a`.
 
 ```rzk
 #def ind-has-section

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

@@ -728,17 +728,15 @@ equivalence.
 ```rzk
 #def is-local-type
   : U
-  :=
-    is-equiv (ψ → A) (ϕ → A) ( \ τ t → τ t)
+  := is-equiv (ψ → A) (ϕ → A) ( \ τ t → τ t)
 ```
 
 We can ask that the terminal map `A → Unit` is right orthogonal to `ϕ ⊂ ψ`.
 
 ```rzk
 #def is-right-orthogonal-terminal-map
   : U
-  :=
-    is-right-orthogonal-to-shape I ψ ϕ A Unit (terminal-map A)
+  := is-right-orthogonal-to-shape I ψ ϕ A Unit (terminal-map A)
 ```
 
 ### Unique extensions types are local types

src/simplicial-hott/07-discrete.rzk.md

@@ -251,9 +251,8 @@ of discrete types is discrete.
 ```
 
 By extension extensionality, an extension type into a family of discrete types
-is discrete. Since `#!rzk equiv-extensions-BOT-equiv` considers total
-extension types only, extending from `#!rzk BOT`, that's all we prove here for
-now.
+is discrete. Since `#!rzk equiv-extensions-BOT-equiv` considers total extension
+types only, extending from `#!rzk BOT`, that's all we prove here for now.
 
 ```rzk
 #def equiv-hom-eq-extension-type-is-discrete uses (extext)