Examples of modalities and various fixes (#639)

### Summary
#### Modalities
- Define `f`-separated types
- Define the following modalities
  - the double negation uniquely eliminating modality
  - the zero uniquely eliminating modality
  - the truncation uniquely eliminating modalities
  - the identity/trivial modality
  - the raise modalities
  - the open higher modalities
  - the closed higher modalities
- Add table of all modalities to the `orthogonal-factorization-systems`
index file
#### VSCode
- Fix snippets for vscode
- Add some more vscode settings for a better user experience and misc.
workspace fixes
#### Styling
- Use bold font instead of italic when defining terms in text
- Some styling of module titles
- Consistent spelling: prefer US English "labeled" over British
"labelled"

.vscode/extensions.json

@@ -8,6 +8,8 @@
     "fredrikbakke.agda-syntax",
     "github.vscode-pull-request-github",
     "ms-python.python",
-    "ms-python.vscode-pylance"
+    "ms-python.vscode-pylance",
+    "oderwat.indent-rainbow",
+    "brunnerh.insert-unicode"
   ]
 }

.vscode/settings.json

@@ -1,7 +1,20 @@
 {
+  "json.schemaDownload.enable": true,
+
   // UI settings
   "breadcrumbs.enabled": false,
 
+  "indentRainbow.indicatorStyle": "light",
+  "indentRainbow.updateDelay": 0,
+
+  "task.problemMatchers.neverPrompt": {
+    "shell": true
+  },
+
+  "editor.unicodeHighlight.ambiguousCharacters": false,
+  "editor.unicodeHighlight.invisibleCharacters": true,
+
+  // File nesting for agda auxillary files
   "explorer.fileNesting.enabled": true,
   "explorer.fileNesting.expand": false,
   "explorer.fileNesting.patterns": {
@@ -11,6 +24,8 @@
   },
 
   // Snippet setup
+  "editor.inlineSuggest.enabled": true,
+  "editor.acceptSuggestionOnEnter": "off",
   "editor.snippetSuggestions": "top",
   "editor.wordBasedSuggestions": false,
   "javascript.suggest.names": false,
@@ -23,6 +38,8 @@
   "files.insertFinalNewline": true,
   "files.trimFinalNewlines": true,
   "files.trimTrailingWhitespace": true,
+
+  // File specific
   "files.associations": {
     "*.agda": "agda",
     "*.lagda.md": "literate agda markdown"
@@ -32,10 +49,11 @@
     "editor.tabSize": 2,
     "editor.rulers": [80],
     "editor.quickSuggestions": {
-      "other": "inline"
+      "other": "on"
     },
     "editor.autoClosingBrackets": "never"
   },
+
   "[css]": {
     "editor.quickSuggestions": {
       "other": true
@@ -44,25 +62,38 @@
     "gitlens.codeLens.scopes": ["document"],
     "editor.tabSize": 2
   },
+
   "[javascript]": {
     "editor.maxTokenizationLineLength": 2500,
     "editor.tabSize": 2
   },
+
   "[json][jsonc]": {
     "editor.quickSuggestions": {
       "strings": true
     },
     "editor.suggest.insertMode": "replace",
     "gitlens.codeLens.scopes": ["document"]
   },
-  "[markdown][literate agda markdown]": {
+
+  "[literate agda markdown]": {
     "editor.tabSize": 2,
     "editor.rulers": [80],
     "editor.quickSuggestions": {
-      "other": "inline"
+      "other": "on"
     },
     "editor.autoClosingBrackets": "never"
   },
+
+  "[markdown]": {
+    "editor.tabSize": 2,
+    "editor.rulers": [80],
+    "editor.quickSuggestions": {
+      "other": "on"
+    },
+    "editor.autoClosingBrackets": "never"
+  },
+
   "[python]": {
     "editor.tabSize": 4,
     "editor.defaultFormatter": "ms-python.python"

.vscode/tasks.json

@@ -17,12 +17,24 @@
       "args": ["pre-commit"],
       "problemMatcher": []
     },
+    {
+      "label": "remove-unused-imports",
+      "detail": "Search for and remove unused imports",
+      "type": "shell",
+      "command": "python",
+      "args": ["${workspaceFolder}/scripts/remove_unused_imports.py"],
+      "problemMatcher": [],
+      "hide": true
+    },
     {
       "label": "unused-imports",
       "detail": "Search for and remove unused imports. Very slow!",
       "type": "shell",
-      "command": "python scripts/remove_unused_imports.py && python scripts/demote_foundation_imports.py",
-      "problemMatcher": []
+      "command": "python",
+      "args": ["${workspaceFolder}/scripts/demote_foundation_imports.py"],
+      "problemMatcher": [],
+      "dependsOn": "remove-unused-imports"
     }
-  ]
+  ],
+  "statusbar.default.hide": false
 }

DESIGN-PRINCIPLES.md

@@ -34,16 +34,14 @@ makes use of several postulates.
 
 Note that there is some redundancy in the postulates we assume. For example, the
 [univalence axiom implies function extensionality](https://unimath.github.io/agda-unimath/foundation.univalence-implies-function-extensionality.html),
-but we still assume function extensionality separately. Furthermore, The
-interval type is contractible, so there is no need at all to postulate it. The
-circle can be constructed as the type of `ℤ`-torsors, and the replacement axiom
-can be used to prove there is a circle in `UU lzero`. Adittionally, the
-replacement axiom can be proven by the join construction, which only uses
-pushouts. Finally, the Agda built-in types do not change the semantics of the
-theory, they only give convenience to the user of the library.
-
-We also note that the higher inductive types in the `agda-unimath` library only
-have computation rules up to identification.
+but we still assume function extensionality separately. Furthermore,
+[the interval type is contractible](synthetic-homotopy-theory.interval-type.md),
+and the higher inductive types in the `agda-unimath` library only have
+computation rules up to identification, so there is no need at all to postulate
+it. The circle can be constructed as the type of `ℤ`-torsors, and the
+replacement axiom can be used to prove there is a circle in `UU lzero`.
+Additionally, the replacement axiom can be proven by the join construction,
+which only uses pushouts.
 
 With these postulates, the `agda-unimath` library is a library for constructive
 univalent mathematics. Mathematics for which the law of excluded middle or the

src/category-theory/yoneda-lemma-precategories.lagda.md

@@ -1,4 +1,4 @@
-# Yoneda lemma for precategories
+# The Yoneda lemma for precategories
 
 ```agda
 module category-theory.yoneda-lemma-precategories where

src/elementary-number-theory/groups-of-modular-arithmetic.lagda.md

@@ -1,4 +1,4 @@
-# The groups ℤ/kℤ
+# The groups `ℤ/kℤ`
 
 ```agda
 module elementary-number-theory.groups-of-modular-arithmetic where

src/elementary-number-theory/powers-of-two.lagda.md

@@ -1,4 +1,4 @@
-# Powers of Two
+# Powers of two
 
 ```agda
 module elementary-number-theory.powers-of-two where

src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md

@@ -1,4 +1,4 @@
-# The Well-Ordering Principle of the standard finite types
+# The well-ordering principle of the standard finite types
 
 ```agda
 module elementary-number-theory.well-ordering-principle-standard-finite-types where
@@ -47,7 +47,7 @@ open import univalent-combinatorics.standard-finite-types
 ## Idea
 
 The standard finite types inherit a well-ordering principle from the natural
-numbers
+numbers.
 
 ## Properties
 
@@ -187,7 +187,7 @@ well-ordering-principle-∃-Fin k P H =
       ( is-decidable-decidable-subtype P))
 ```
 
-### Hilbert's epsilon operator for decidable subtypes of standard finite types
+### Hilbert's `ε`-operator for decidable subtypes of standard finite types
 
 ```agda
 ε-operator-decidable-subtype-Fin :

src/finite-group-theory/abstract-quaternion-group.lagda.md

@@ -1,4 +1,4 @@
-# The abstract quaternion group of order 8
+# The abstract quaternion group of order `8`
 
 ```agda
 module finite-group-theory.abstract-quaternion-group where

src/finite-group-theory/concrete-quaternion-group.lagda.md

@@ -82,53 +82,53 @@ equiv-face-cube k X Y e d a =
         ( inclusion-complement-point-UU-Fin k
           ( pair (dim-cube-UU-Fin (succ-ℕ k) X) d) d')))
 
-cube-with-labelled-faces :
+cube-with-labeled-faces :
   (k : ℕ) → UU (lsuc lzero)
-cube-with-labelled-faces k =
+cube-with-labeled-faces k =
   Σ ( cube (succ-ℕ k))
     ( λ X →
       (d : dim-cube (succ-ℕ k) X) (a : axis-cube (succ-ℕ k) X d) →
       labelling-cube k (face-cube k X d a))
 
-cube-cube-with-labelled-faces :
-  (k : ℕ) → cube-with-labelled-faces k → cube (succ-ℕ k)
-cube-cube-with-labelled-faces k X = pr1 X
+cube-cube-with-labeled-faces :
+  (k : ℕ) → cube-with-labeled-faces k → cube (succ-ℕ k)
+cube-cube-with-labeled-faces k X = pr1 X
 
-labelling-faces-cube-with-labelled-faces :
-  (k : ℕ) (X : cube-with-labelled-faces k)
-  (d : dim-cube (succ-ℕ k) (cube-cube-with-labelled-faces k X))
-  (a : axis-cube (succ-ℕ k) (cube-cube-with-labelled-faces k X) d) →
-  labelling-cube k (face-cube k (cube-cube-with-labelled-faces k X) d a)
-labelling-faces-cube-with-labelled-faces k X = pr2 X
+labelling-faces-cube-with-labeled-faces :
+  (k : ℕ) (X : cube-with-labeled-faces k)
+  (d : dim-cube (succ-ℕ k) (cube-cube-with-labeled-faces k X))
+  (a : axis-cube (succ-ℕ k) (cube-cube-with-labeled-faces k X) d) →
+  labelling-cube k (face-cube k (cube-cube-with-labeled-faces k X) d a)
+labelling-faces-cube-with-labeled-faces k X = pr2 X
 
 {-
-standard-cube-with-labelled-faces :
-  (k : ℕ) → cube-with-labelled-faces k
-standard-cube-with-labelled-faces k =
+standard-cube-with-labeled-faces :
+  (k : ℕ) → cube-with-labeled-faces k
+standard-cube-with-labeled-faces k =
   pair ( standard-cube (succ-ℕ k))
        ( λ d a → {!!})
 -}
 
-equiv-cube-with-labelled-faces :
-  {k : ℕ} (X Y : cube-with-labelled-faces k) → UU lzero
-equiv-cube-with-labelled-faces {k} X Y =
+equiv-cube-with-labeled-faces :
+  {k : ℕ} (X Y : cube-with-labeled-faces k) → UU lzero
+equiv-cube-with-labeled-faces {k} X Y =
   Σ ( equiv-cube (succ-ℕ k)
-      ( cube-cube-with-labelled-faces k X)
-      ( cube-cube-with-labelled-faces k Y))
-    ( λ e → ( d : dim-cube (succ-ℕ k) (cube-cube-with-labelled-faces k X))
-            ( a : axis-cube (succ-ℕ k) (cube-cube-with-labelled-faces k X) d) →
+      ( cube-cube-with-labeled-faces k X)
+      ( cube-cube-with-labeled-faces k Y))
+    ( λ e → ( d : dim-cube (succ-ℕ k) (cube-cube-with-labeled-faces k X))
+            ( a : axis-cube (succ-ℕ k) (cube-cube-with-labeled-faces k X) d) →
             htpy-equiv-cube k
               ( standard-cube k)
               ( face-cube k
-                ( cube-cube-with-labelled-faces k Y)
+                ( cube-cube-with-labeled-faces k Y)
                 ( map-dim-equiv-cube (succ-ℕ k)
-                  ( cube-cube-with-labelled-faces k X)
-                  ( cube-cube-with-labelled-faces k Y)
+                  ( cube-cube-with-labeled-faces k X)
+                  ( cube-cube-with-labeled-faces k Y)
                   ( e)
                   ( d))
                 ( map-axis-equiv-cube (succ-ℕ k)
-                  ( cube-cube-with-labelled-faces k X)
-                  ( cube-cube-with-labelled-faces k Y)
+                  ( cube-cube-with-labeled-faces k X)
+                  ( cube-cube-with-labeled-faces k Y)
                   e d a))
               ( comp-equiv-cube k
                 ( standard-cube k)
@@ -137,14 +137,14 @@ equiv-cube-with-labelled-faces {k} X Y =
                   ( map-dim-equiv-cube (succ-ℕ k) (pr1 X) (pr1 Y) e d)
                   ( map-axis-equiv-cube (succ-ℕ k) (pr1 X) (pr1 Y) e d a))
                 ( equiv-face-cube k (pr1 X) (pr1 Y) e d a)
-                ( labelling-faces-cube-with-labelled-faces k X d a))
-              ( labelling-faces-cube-with-labelled-faces k Y
+                ( labelling-faces-cube-with-labeled-faces k X d a))
+              ( labelling-faces-cube-with-labeled-faces k Y
                 ( map-dim-equiv-cube (succ-ℕ k)
-                  ( cube-cube-with-labelled-faces k X)
-                  ( cube-cube-with-labelled-faces k Y)
+                  ( cube-cube-with-labeled-faces k X)
+                  ( cube-cube-with-labeled-faces k Y)
                   e d)
                 ( map-axis-equiv-cube (succ-ℕ k)
-                  ( cube-cube-with-labelled-faces k X)
-                  ( cube-cube-with-labelled-faces k Y)
+                  ( cube-cube-with-labeled-faces k X)
+                  ( cube-cube-with-labeled-faces k Y)
                   e d a)))
 ```

src/finite-group-theory/groups-of-order-2.lagda.md

@@ -1,4 +1,4 @@
-# Groups of order 2
+# Groups of order `2`
 
 ```agda
 {-# OPTIONS --lossy-unification #-}

src/finite-group-theory/tetrahedra-in-3-space.lagda.md

@@ -1,4 +1,4 @@
-# Tetrahedra in 3-dimensional space
+# Tetrahedra in `3`-dimensional space
 
 ```agda
 module finite-group-theory.tetrahedra-in-3-space where

src/foundation-core/1-types.lagda.md

@@ -1,4 +1,4 @@
-# 1-Types
+# `1`-Types
 
 ```agda
 module foundation-core.1-types where

src/foundation-core/homotopies.lagda.md

@@ -31,6 +31,7 @@ module _
 
   eq-value : X → UU l2
   eq-value x = (f x ＝ g x)
+  {-# INLINE eq-value #-}
 
   map-compute-path-over-eq-value :
     {x y : X} (p : x ＝ y) (q : eq-value x) (r : eq-value y) →

src/foundation-core/path-split-maps.lagda.md

@@ -22,10 +22,13 @@ open import foundation-core.sections
 
 ## Idea
 
-A map `f : A → B` is said to be path split if it has a section and its action on
-identity types `Id x y → Id (f x) (f y)` has a section for each `x y : A`. By
-the fundamental theorem for identity types, it follows that a map is path-split
-if and only if it is an equivalence.
+A map `f : A → B` is said to be **path split** if it has a
+[section](foundation-core.sections.md) and its action on
+[identity types](foundation-core.identity-types.md) `Id x y → Id (f x) (f y)`
+has a section for each `x y : A`. By the
+[fundamental theorem of identity types](foundation-core.fundamental-theorem-of-identity-types.md),
+it follows that a map is path-split if and only if it is an
+[equivalence](foundation-core.equivalences.md).
 
 ## Definition
 
@@ -90,3 +93,13 @@ module _
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of maps with contractible fibers see
   [`foundation.contractible-maps`](foundation.contractible-maps.md).
+
+## References
+
+- Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations
+  of Mathematics_ (2013) (<https://homotopytypetheory.org/book/>,
+  [arXiv:1308.0729](https://arxiv.org/abs/1308.0729),
+  [DOI:10.48550](https://doi.org/10.48550/arXiv.1308.0729))
+- Mike Shulman, _Universal properties without function extensionality_
+  (November 2014)
+  ([HoTT Blog](https://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/))

src/foundation-core/propositions.lagda.md

@@ -277,7 +277,7 @@ abstract
   is-prop-function-type :
     {l1 l2 : Level} {A : UU l1} {B : UU l2} →
     is-prop B → is-prop (A → B)
-  is-prop-function-type H = is-prop-Π (λ x → H)
+  is-prop-function-type H = is-prop-Π (λ _ → H)
 
 type-function-Prop :
   {l1 l2 : Level} → UU l1 → Prop l2 → UU (l1 ⊔ l2)