Revert "format files"

This reverts commit d47e9ff.

.vscode/extensions.json

@@ -1,6 +1,6 @@
 {
-  "recommendations": [
-    "nikolaikudasovfizruk.rzk-1-experimental-highlighting",
-    "esbenp.prettier-vscode"
-  ]
+    "recommendations": [
+        "nikolaikudasovfizruk.rzk-1-experimental-highlighting",
+        "esbenp.prettier-vscode"
+    ]
 }

src/hott/06-contractible.rzk.md

@@ -533,52 +533,48 @@ A type is contractible if and only if it has singleton induction.
 
 ## Identity types of contractible types
 
-We show that any two paths between the same endpoints in a contractible type are
-the same.
-
-In a contractible type any path $p : x = y$ is equal to the path constructed in
-`eq-is-contr`.
+We show that any two paths between the same endpoints in a contractible type are the same. 
 
+In a contractible type any path $p : x = y$ is equal to the path constructed in `eq-is-contr`. 
 ```rzk
 #define path-eq-path-through-center-is-contr
   ( A : U)
   ( is-contr-A : is-contr A)
   ( x y : A)
   ( p : x = y)
   : ((eq-is-contr A is-contr-A x y) = p)
-  :=
+  := 
     ind-path
     ( A)
     ( x)
-    ( \ y' p' → (eq-is-contr A is-contr-A x y') = p')
-    ( left-inverse-concat A (center-contraction A is-contr-A) x (homotopy-contraction A is-contr-A x))
-    ( y)
-    ( p)
+    ( \ y' p' → (eq-is-contr A is-contr-A x y') = p') 
+    ( left-inverse-concat A (center-contraction A is-contr-A) x (homotopy-contraction A is-contr-A x)) 
+    ( y) 
+    ( p) 
 
 ```
 
-Finally, in a contractible type any two paths between the same end points are
-equal. There are many possible proofs of this (e.g. identifying contractible
-types with the unit type where it is more transparent), but we proceed by gluing
-together the two identifications to the out and back path.
+Finally, in a contractible type any two paths between the same end points are equal. There are many possible proofs of this (e.g. identifying contractible types with the unit type where it is more transparent), but we proceed by gluing together the two identifications to the out and back path.
 
 ```rzk
-#define all-paths-eq-is-contr
+#define all-paths-eq-is-contr 
  ( A : U)
  ( is-contr-A : is-contr A)
  ( x y : A)
- ( p q : x = y)
+ ( p q : x = y) 
  : (p = q)
- :=
+ := 
   concat
     ( x = y)
     ( p)
     ( eq-is-contr A is-contr-A x y)
     ( q)
     ( rev
-      (x = y)
+      (x = y) 
       ( eq-is-contr A is-contr-A x y)
-      ( p)
+      ( p) 
       ( path-eq-path-through-center-is-contr A is-contr-A x y p))
     ( path-eq-path-through-center-is-contr A is-contr-A x y q)
 ```
+
+

src/hott/11-homotopy-pullbacks.rzk.md

@@ -8,9 +8,8 @@ This is a literate `rzk` file:
 
 ## Homotopy cartesian squares
 
-We start by fixing the data of a map between two type families `A' → U` and
-`A → U`, which we think of as a commutative square
-
+We start by fixing the data of a map between two type families
+`A' → U` and `A → U`, which we think of as a commutative square
 ```
 Σ A' → Σ A
  ↓      ↓
@@ -36,8 +35,8 @@ We start by fixing the data of a map between two type families `A' → U` and
   := \ (a', c') → (α a', γ a' c')
 ```
 
-We say that such a square is homotopy cartesian just if it induces an
-equivalence componentwise.
+We say that such a square is homotopy cartesian
+just if it induces an equivalence componentwise.
 
 ```rzk
 #def is-homotopy-cartesian uses (A)
@@ -217,8 +216,8 @@ always do this (whether the square is homotopy-cartesian or not).
 
 ### Invariance under pullbacks
 
-We can pullback a homotopy cartesian square over `α : A' → A` along any map of
-maps `β → α` and obtain another homotopy cartesian square.
+We can pullback a homotopy cartesian square over `α : A' → A`
+along any map of maps `β → α` and obtain another homotopy cartesian square.
 
 ```rzk
 #def is-homotopy-cartesian-pullback
@@ -247,15 +246,16 @@ maps `β → α` and obtain another homotopy cartesian square.
 
 ## Pasting calculus for homotopy cartesian squares
 
-Currently our notion of squares is not symmetric, since the vertical maps are
-given by type families, i.e. they are _display maps_, while the horizontal maps
-are arbitrary. Therefore we distinquish between the vertical and the horizontal
-pasting calculus.
+Currently our notion of squares is not symmetric,
+since the vertical maps are given by type families,
+i.e. they are _display maps_,
+while the horizontal maps are arbitrary.
+Therefore we distinquish between the vertical and the horizontal pasting calculus.
 
 ### Vertical calculus
 
-The following vertical composition and cancellation laws follow easily from the
-corresponding statements about equivalences established above.
+The following vertical composition and cancellation laws follow easily from
+the corresponding statements about equivalences established above.
 
 ```rzk
 #section homotopy-cartesian-vertical-calculus

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

@@ -17,12 +17,13 @@ This is a literate `rzk` file:
 
 ## Extension up to homotopy
 
-For a shape inclusion `ϕ ⊂ ψ` and any type `A`, we have the inbuilt extension
-types `(t : ψ) → A [ϕ t ↦ σ t]` (for every `σ : ϕ → A`).
+For a shape inclusion `ϕ ⊂ ψ` and any type `A`,
+we have the inbuilt extension types `(t : ψ) → A [ϕ t ↦ σ t]`
+(for every `σ : ϕ → A`).
 
-We show that these extension types are equivalent to the fibers of the canonical
-restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of
-"extension up to homotopy".
+We show that these extension types are equivalent to the fibers
+of the canonical restriction map `(ψ → A) → (ϕ → A)`,
+which we can view as the types  of "extension up to homotopy".
 
 ```rzk
 #section extensions-up-to-homotopy

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

@@ -16,26 +16,26 @@ Some of the definitions in this file rely on naive extension extensionality:
 
 ## Right orthogonal maps with respect to shapes
 
-For every shape inclusion `ϕ ⊂ ψ`, we obtain a fibrancy condition for a map
-`α : A' → A` in terms of unique extension along `ϕ ⊂ ψ`. This is a relative
-version of unique extension along `ϕ ⊂ ψ`.
+For every shape inclusion `ϕ ⊂ ψ`,
+we obtain a fibrancy condition for a map `α : A' → A`
+in terms of unique extension along `ϕ ⊂ ψ`.
+This is a relative version of unique extension along `ϕ ⊂ ψ`.
 
 We say that `α : A' → A` is _right orthogonal_ to the shape inclusion `ϕ ⊂ ψ`,
 if the square
-
 ```
 (ψ → A') → (ψ → A)
 
    ↓          ↓
 
 (ϕ → A') → (ϕ → A)
 ```
-
 is homotopy cartesian.
 
-Equivalently, we can interpret this orthogonality as a cofibrancy condition on
-the shape inclusion. We say that the shape inclusion `ϕ ⊂ ψ` is _left
-orthogonal_ to the map `α`, if `α : A' → A` is right orthogonal to `ϕ ⊂ ψ`.
+Equivalently, we can interpret this orthogonality
+as a cofibrancy condition on the shape inclusion.
+We say that the shape inclusion `ϕ ⊂ ψ` is _left orthogonal_ to the map `α`,
+if `α : A' → A` is right orthogonal to `ϕ ⊂ ψ`.
 
 ```rzk title="BW23, Section 3"
 #def is-right-orthogonal-to-shape
@@ -62,9 +62,8 @@ We fix a map `α : A' → A`.
 #variables A' A : U
 #variable α : A' → A
 ```
-
-Consider nested shapes `ϕ ⊂ χ ⊂ ψ` and the three possible right orthogonality
-conditions.
+Consider nested shapes `ϕ ⊂ χ ⊂ ψ`
+and the three possible right orthogonality conditions.
 
 ```rzk
 #variable I : CUBE
@@ -78,18 +77,19 @@ conditions.
   -- rzk does not accept these terms after η-reduction
 ```
 
-Using the vertical pasting calculus for homotopy cartesian squares, it is not
-hard to deduce the corresponding composition and cancellation properties for
-left orthogonality of shape inclusion with respect to `α : A' → A`.
+Using the vertical pasting calculus for homotopy cartesian squares,
+it is not hard to deduce the corresponding composition and cancellation properties
+for left orthogonality of shape inclusion with respect to `α : A' → A`.
 
 ### Σ over an intermediate shape
 
-The only fact that stops some of these laws from being a direct corollary is
-that the `Σ`-types appearing in the vertical pasting of the relevant squares
-(such as `Σ (\ σ : ϕ → A), ( (t : χ) → A [ϕ t ↦ σ t])`) are not literally equal
-to the corresponding extension types (such as `τ → A `). Therefore we have to
-occasionally go back or forth along the functorial equivalence
-`cofibration-composition-functorial`.
+The only fact that stops some of these laws from being a direct corollary
+is that the `Σ`-types appearing in the vertical pasting of the relevant squares
+(such as `Σ (\ σ : ϕ → A), ( (t : χ) → A [ϕ t ↦ σ t])`)
+are not literally equal to the corresponding extension types
+(such as `τ → A `).
+Therefore we have to occasionally go back or forth along the
+functorial equivalence `cofibration-composition-functorial`.
 
 ```rzk
 #def is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape uses (is-orth-ψ-ϕ)
@@ -177,8 +177,9 @@ If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so i
           τ'
 ```
 
-If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` and `χ ⊂ ψ` is a (functorial)
-shape retract, then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`.
+If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`
+and `χ ⊂ ψ` is a (functorial) shape retract,
+then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`.
 
 ```rzk
 #def is-right-orthogonal-to-shape-right-cancel-retract uses (is-orth-ψ-ϕ)
@@ -203,11 +204,11 @@ shape retract, then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`.
 
 ### Stability under exponentiation
 
-If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` then so is `χ × ϕ ⊂ χ × ψ` for
-every other shape `χ`.
+If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`
+then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`.
 
-The following proof uses a lot of currying and uncurrying and relies on (the
-naive form of) extension extensionality.
+The following proof uses a lot of currying and uncurrying
+and relies on (the naive form of) extension extensionality.
 
 ```rzk
 #def is-right-orthogonal-to-shape-× uses (naiveextext)
@@ -279,8 +280,8 @@ naive form of) extension extensionality.
 
 ### Stability under exact pushouts
 
-For any two shapes `ϕ, ψ ⊂ I`, if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to
-`α : A' → A`, then so is `ψ ⊂ ϕ ∪ ψ`.
+For any two shapes `ϕ, ψ ⊂ I`, if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to `α : A' → A`,
+then so is `ψ ⊂ ϕ ∪ ψ`.
 
 ```rzk
 #def is-right-orthogonal-to-shape-pushout
@@ -304,8 +305,8 @@ For any two shapes `ϕ, ψ ⊂ I`, if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to
 
 ## Types with unique extension
 
-We say that an type `A` has unique extensions for a shape inclusion `ϕ ⊂ ψ`, if
-for each `σ : ϕ → A` the type of `ψ`-extensions is contractible.
+We say that an type `A` has unique extensions for a shape inclusion `ϕ ⊂ ψ`,
+if for each `σ : ϕ → A` the type of `ψ`-extensions is contractible.
 
 ```rzk
 #def has-unique-extensions
@@ -318,8 +319,8 @@ for each `σ : ϕ → A` the type of `ψ`-extensions is contractible.
     ( σ : ϕ → A) → is-contr ( (t : ψ) → A [ϕ t ↦ σ t])
 ```
 
-The property of having unique extension can be pulled back along any right
-orthogonal map.
+The property of having unique extension
+can be pulled back along any right orthogonal map.
 
 ```rzk
 #def has-unique-extensions-domain-right-orthogonal-has-unique-extensions-codomain
@@ -355,9 +356,9 @@ is an equivalence.
     is-equiv (ψ → A) (ϕ → A) ( \ τ t → τ t)
 ```
 
-This follows straightforwardly from the fact that for every `σ : ϕ → A` we have
-an equivalence between the extension type `(t : ψ) → A [ϕ t ↦ σ t]` and the
-fiber of the restriction map `(ψ → A) → (ϕ → A)`.
+This follows straightforwardly from the fact that for every `σ : ϕ → A`
+we have an equivalence between the extension type `(t : ψ) → A [ϕ t ↦ σ t]`
+and the fiber of the restriction map `(ψ → A) → (ϕ → A)`.
 
 ```rzk
 #def is-local-type-has-unique-extensions
@@ -388,8 +389,8 @@ fiber of the restriction map `(ψ → A) → (ϕ → A)`.
 #end is-local-type
 ```
 
-Since the property of having unique extensions passes from the codomain to the
-domain of a right orthogonal map, the same is true for locality of types.
+Since the property of having unique extensions passes from the codomain to the domain
+of a right orthogonal map, the same is true for locality of types.
 
 ```rzk
 #def is-local-type-domain-right-orthogonal-is-local-type-codomain

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

@@ -16,8 +16,8 @@ This is a literate `rzk` file:
 - `hott/total-space.md` — We rely on
   `#!rzk is-equiv-projection-contractible-fibers` and
   `#!rzk projection-total-type` in the proof of Theorem 5.5.
-- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and
-  their subshapes.
+- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and their
+  subshapes.
 - `03-extension-types.rzk.md` — We use the fubini theorem and extension
   extensionality.
 
@@ -1779,8 +1779,8 @@ The cofibration Λ²₁ → Δ² is inner anodyne
 
 ## Inner fibrations
 
-An inner fibration is a map `α : A' → A` which is right orthogonal to `Λ ⊂ Δ²`.
-This is the relative notion of a Segal type.
+An inner fibration is a map `α : A' → A` which is right orthogonal
+to `Λ ⊂ Δ²`. This is the relative notion of a Segal type.
 
 ```rzk
 #def is-inner-fibration