Update prettier pre-commit hook

Though it's deprecated now, and apparently there is no supporter way
to run prettier from pre-commit.

It also now considers some arrow characters double-width, since
Unicode classifies them as emojis; though I don't think it's worth it
to fight prettier on it

Author: VojtechStep

.pre-commit-config.yaml

@@ -138,7 +138,7 @@ repos:
         args: ['-i', '--global-config', '/dev/null']
 
   - repo: https://github.com/pre-commit/mirrors-prettier
-    rev: 'v3.0.0-alpha.6'
+    rev: 'v4.0.0-alpha.8'
     hooks:
       - id: prettier
         name: CSS, JS, YAML and Markdown (no codeblocks) formatting

CODINGSTYLE.md

@@ -110,7 +110,6 @@ agda-unimath project.
   definition. This contradicts our objective of organizing the library into
   compact, reusable components. If a `where` block is deemed necessary, follow
   these conventions:
-
   - Opt for `where` blocks over `let` expressions.
   - Indent the `where` keyword by two spaces and align their content with the
     `where` keyword.
@@ -136,7 +135,6 @@ agda-unimath project.
 
   There are multiple syntaxes for writing lambda expressions in Agda. Generally,
   you have the following options:
-
   1. Regular lambda expressions without pattern matching:
 
      ```agda
@@ -402,7 +400,6 @@ library:
 - In order to improve the readability on the agda-unimath website, we use a
   standard line length of 80 characters. There are only a few exceptions that
   enable us to have names that are more than 80 characters long:
-
   - Named `module` declarations
   - `open import` statements
   - Lines consisting of a single, possibly parenthesized (`(){}`), token that is

HOWTO-INSTALL.md

@@ -392,7 +392,6 @@ This issue can arise if the `pre-commit` executable gets placed in the
    `ls ~/.local/bin | grep pre-commit` to see if the executable is present.
 
 2. **Update your `PATH`**:
-
    - If you're using the bash terminal, open your `.bashrc` file with a text
      editor like `nano`:
 
@@ -409,7 +408,6 @@ This issue can arise if the `pre-commit` executable gets placed in the
    - Save the file and close the editor.
 
 3. **Reload your `.bashrc`**:
-
    - Run the following command to apply the changes:
 
      ```bash

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/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/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`              |

theme/css/chrome.css

@@ -158,13 +158,17 @@ a > .hljs {
   align-content: center;
   flex-direction: column;
 
-  transition: color 0.5s, background-color 0.5s;
+  transition:
+    color 0.5s,
+    background-color 0.5s;
 }
 
 .nav-chapters:hover {
   text-decoration: none;
   background-color: var(--theme-hover);
-  transition: background-color 0.15s, color 0.15s;
+  transition:
+    background-color 0.15s,
+    color 0.15s;
 }
 
 .nav-wrapper {
@@ -240,7 +244,9 @@ pre > .buttons {
   cursor: pointer;
   visibility: hidden;
   opacity: 0;
-  transition: visibility 0.1s linear, opacity 0.1s linear;
+  transition:
+    visibility 0.1s linear,
+    opacity 0.1s linear;
 }
 pre:hover > .buttons {
   visibility: visible;

theme/css/general.css

@@ -110,7 +110,9 @@ h6:target::before {
   box-sizing: border-box;
 }
 .js:not(.sidebar-resizing) .page-wrapper {
-  transition: margin-left 0.3s ease, transform 0.3s ease; /* Animation: slide away */
+  transition:
+    margin-left 0.3s ease,
+    transform 0.3s ease; /* Animation: slide away */
 }
 
 .content {

theme/css/variables.css

@@ -5,9 +5,9 @@
   --page-padding: 5px;
   --content-max-width: 75%;
   --menu-bar-height: 40px;
-  --mono-font: Menlo, Source Code Pro, Consolas, Monaco, Lucida Console,
-    Liberation Mono, DejaVu Sans Mono, Bitstream Vera Sans Mono, Courier New,
-    monospace;
+  --mono-font:
+    Menlo, Source Code Pro, Consolas, Monaco, Lucida Console, Liberation Mono,
+    DejaVu Sans Mono, Bitstream Vera Sans Mono, Courier New, monospace;
   --code-font-size: 1.3rem;
   --pagetoc-fontsize: 0.85em;
 }