chore: New Prettier formatting (#1733)

Resolves #1731.

Author: fredrik-bakke

docs/MIXFIX-OPERATORS.md

@@ -177,8 +177,8 @@ Below, we outline a list of general rules when assigning associativities.
 | 16               | Right homotopy whiskering `_·r_`                                                                                                                                                                   |
 | 15               | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, `_*_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, concatenation operators like `_∙_` and `_∙h_` |
 | 10               | Parametric additive operators like `_+_`, `_∨_`, `_∨∗_`, list concatenation, monadic bind operators for the type checking monad                                                                    |
-| 6                | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, `_⇔_`, and `_↔_`, elementhood relations, subtype relations                                                                             |
-| 5                | Directed function type-like formation operators, e.g. `_⇒_`, `_↪_`, `_→∗_`, `_↠_`, `_↪ᵈ_`, and `_⊆_`                                                                                             |
+| 6                | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, `_⇔_`, and `_↔_`, elementhood relations, subtype relations                                                                              |
+| 5                | Directed function type-like formation operators, e.g. `_⇒_`, `_↪_`, `_→∗_`, `_↠_`, `_↪ᵈ_`, and `_⊆_`                                                                                               |
 | 3                | The pairing operators `_,_` and `_,ω_`                                                                                                                                                             |
 | 0-1              | Reasoning syntaxes                                                                                                                                                                                 |
 | -∞               | Function type formation `_→_`                                                                                                                                                                      |

src/foundation-core/propositions.lagda.md

@@ -417,7 +417,7 @@ $n$-[types](foundation-core.truncated-types.md).
 | [Dependent sum](foundation.dependent-pair-types.md)         | `Σ`               | `Σ-Prop`                          |
 | [Dependent product](foundation.dependent-function-types.md) | `Π`               | `Π-Prop`                          |
 | [Functions](foundation-core.function-types.md)              | `→`               | `⇒`                               |
-| [Logical equivalence](foundation.logical-equivalences.md)   | `↔`              | `⇔`                               |
+| [Logical equivalence](foundation.logical-equivalences.md)   | `↔`               | `⇔`                               |
 | [Product](foundation-core.cartesian-product-types.md)       | `×`               | `product-Prop`                    |
 | [Join](synthetic-homotopy-theory.joins-of-types.md)         | `*`               | `join-Prop`                       |
 | [Exclusive sum](foundation.exclusive-sum.md)                | `exclusive-sum`   | `exclusive-sum-Prop`              |

src/foundation/cantor-schroder-bernstein-decidable-embeddings.lagda.md

@@ -284,8 +284,8 @@ module _
 ## Theorem
 
 It follows from the weak limited principle of omniscience that, for every pair
-of mutual decidable embeddings `f : A ↪ B` and `g : B ↪ A`, it is decidable
-for every element `x : A` whether `x` is a perfect image of `g` relative to `f`.
+of mutual decidable embeddings `f : A ↪ B` and `g : B ↪ A`, it is decidable for
+every element `x : A` whether `x` is a perfect image of `g` relative to `f`.
 Applying this fact to the Cantor-Schröder-Bernstein construction, we conclude
 with the main result.
 

src/foundation/equivalences.lagda.md

@@ -49,8 +49,8 @@ open import foundation-core.type-theoretic-principle-of-choice
 ### Any equivalence is an embedding
 
 We already proved in `foundation-core.equivalences` that equivalences are
-embeddings. Here we have `_↪_` available, so we record the map from
-equivalences to embeddings.
+embeddings. Here we have `_↪_` available, so we record the map from equivalences
+to embeddings.
 
 ```agda
 module _

src/foundation/perfect-images.lagda.md

@@ -64,8 +64,8 @@ of `g`.
 
 This concept is used in the
 [Cantor–Schröder–Bernstein construction](foundation.cantor-schroder-bernstein-decidable-embeddings.md)
-to construct an equivalence of types `A ≃ B` given mutual embeddings
-`f : A ↪ B` and `g : B ↪ A`.
+to construct an equivalence of types `A ≃ B` given mutual embeddings `f : A ↪ B`
+and `g : B ↪ A`.
 
 ## Definitions
 
@@ -478,9 +478,9 @@ module _
 
 It follows from the
 [weak limited principle of omniscience](foundation.weak-limited-principle-of-omniscience.md)
-that, for every pair of mutual decidable embeddings `f : A ↪ B` and
-`g : B ↪ A`, it is decidable for every element `x : A` whether `x` is a perfect
-image of `g` relative to `f`.
+that, for every pair of mutual decidable embeddings `f : A ↪ B` and `g : B ↪ A`,
+it is decidable for every element `x : A` whether `x` is a perfect image of `g`
+relative to `f`.
 
 ```agda
 module _

src/foundation/propositions.lagda.md

@@ -116,7 +116,7 @@ $n$-[types](foundation-core.truncated-types.md).
 | [Dependent sum](foundation.dependent-pair-types.md)         | `Σ`               | `Σ-Prop`                          |
 | [Dependent product](foundation.dependent-function-types.md) | `Π`               | `Π-Prop`                          |
 | [Functions](foundation-core.function-types.md)              | `→`               | `⇒`                               |
-| [Logical equivalence](foundation.logical-equivalences.md)   | `↔`              | `⇔`                               |
+| [Logical equivalence](foundation.logical-equivalences.md)   | `↔`               | `⇔`                               |
 | [Product](foundation-core.cartesian-product-types.md)       | `×`               | `product-Prop`                    |
 | [Join](synthetic-homotopy-theory.joins-of-types.md)         | `*`               | `join-Prop`                       |
 | [Exclusive sum](foundation.exclusive-sum.md)                | `exclusive-sum`   | `exclusive-sum-Prop`              |