Formatting fixes (#530)

Just a bunch of miscellaneous formatting. - Fix capitalization of module titles - Make comment headers into actual headers - Remove some superfluous whitespace - Organize VSCode settings - Add VSCode settings that nest ".agdai" and ".agda~" files under the associated ".lagda.md" file to declutter the file view. - Fix a breaking bug with `generate_main_index` when there are duplicate titles - Add `<details>` blocks to all files (except `foundation-core.universe-levels`) - Remove unused imports
UniMath · Mar 21, 2023 · ccbaa46 · ccbaa46
1 parent 1fc1bce
commit ccbaa46
Show file tree

Hide file tree

Showing 215 changed files with 823 additions and 642 deletions.
diff --git a/.prettierrc.json b/.prettierrc.json
@@ -1,19 +1,19 @@
 {
-	"arrowParens": "always",
-	"bracketSameLine": false,
-	"bracketSpacing": true,
-	"embeddedLanguageFormatting": "off",
-	"htmlWhitespaceSensitivity": "css",
-	"insertPragma": false,
-	"jsxSingleQuote": false,
-	"printWidth": 80,
-	"proseWrap": "always",
-	"quoteProps": "as-needed",
-	"requirePragma": false,
-	"semi": true,
-	"singleAttributePerLine": false,
-	"singleQuote": false,
-	"tabWidth": 2,
-	"trailingComma": "es5",
-	"useTabs": false
+  "arrowParens": "always",
+  "bracketSameLine": false,
+  "bracketSpacing": true,
+  "embeddedLanguageFormatting": "off",
+  "htmlWhitespaceSensitivity": "css",
+  "insertPragma": false,
+  "jsxSingleQuote": false,
+  "printWidth": 80,
+  "proseWrap": "always",
+  "quoteProps": "as-needed",
+  "requirePragma": false,
+  "semi": true,
+  "singleAttributePerLine": false,
+  "singleQuote": false,
+  "tabWidth": 2,
+  "trailingComma": "es5",
+  "useTabs": false
 }
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -1,41 +1,63 @@
 {
+  // UI settings
   "breadcrumbs.enabled": false,
+
+  "explorer.fileNesting.enabled": true,
+  "explorer.fileNesting.expand": false,
+  "explorer.fileNesting.patterns": {
+    "*.agda": "${capture}.agdai, ${capture}.agda~",
+    "*.lagda": "${capture}.agdai, ${capture}.agda~",
+    "*.lagda.md": "${capture}.agdai, ${capture}.agda~"
+  },
+
+  // Snippet setup
   "editor.quickSuggestions": {
     "other": "inline"
   },
   "editor.snippetSuggestions": "top",
   "editor.wordBasedSuggestions": false,
+  "javascript.suggest.names": false,
+
+  // Autoformatting and file type specific settings
+  "editor.defaultFormatter": "esbenp.prettier-vscode",
+  "editor.formatOnType": true,
+  "editor.formatOnSave": true,
+
+  "files.insertFinalNewline": true,
   "files.trimFinalNewlines": true,
   "files.trimTrailingWhitespace": true,
-  "javascript.suggest.names": false,
+
   "[agda]": {
     "editor.tabSize": 2,
     "editor.rulers": [80],
     "editor.formatOnType": true,
     "editor.formatOnSave": true
   },
+  "[css]": {
+    "editor.quickSuggestions": {
+      "other": true
+    },
+    "editor.suggest.insertMode": "replace",
+    "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"],
-    "editor.defaultFormatter": "esbenp.prettier-vscode",
-    "editor.formatOnType": true,
-    "editor.formatOnSave": true
+    "gitlens.codeLens.scopes": ["document"]
   },
   "[markdown]": {
     "editor.tabSize": 2,
-    "editor.rulers": [80],
-    "editor.defaultFormatter": "esbenp.prettier-vscode",
-    "editor.formatOnType": true,
-    "editor.formatOnSave": true
+    "editor.rulers": [80]
   },
   "[python]": {
     "editor.tabSize": 4,
-    "editor.defaultFormatter": "ms-python.python",
-    "editor.formatOnType": true,
-    "editor.formatOnSave": true
-  },
-  "files.insertFinalNewline": true
+    "editor.defaultFormatter": "ms-python.python"
+  }
 }
diff --git a/Makefile b/Makefile
@@ -28,7 +28,7 @@ METAFILES:=CITATION.cff \
 agdaFiles :
 	@rm -rf $@
 	@rm -rf src/everything.lagda.md
-	@find src -name temp -prune -o -type f \( -name "*.agda" -o -name "*.lagda"  -o -name  "*.lagda.md" \) -print > $@
+	@find src -name temp -prune -o -type f \( -name "*.agda" -o -name "*.lagda" -o -name "*.lagda.md" \) -print > $@
 	@sort -o $@ $@
 	@wc -l $@
 	@echo "$(shell (find src -name '*.lagda.md' -print0 | xargs -0 cat ) | wc -l) LOC"

diff --git a/grant-acknowledgements.md b/grant-acknowledgements.md
@@ -1,4 +1,4 @@
-# Grant Acknowledgements
+# Grant acknowledgements
 
 - The [TydiForm project](https://tydiform.fmf.uni-lj.si) (2020-Present). Air
   Force Office of Scientific Research, award number FA9550-21-1-0024.
diff --git a/scripts/demote_foundation_imports.py b/scripts/demote_foundation_imports.py
@@ -17,15 +17,15 @@ def process_agda_file(agda_file, agda_options, root, temp_dir):
 
     if nonpublic is None:
         utils.multithread.thread_safe_print(
-            f"'{agda_module}' Could not find imports. Skipping.")
+            f"'{agda_module}' Could not find imports.")
         return
 
         # Subdivide imports into namespaces
     namespaces = subdivide_namespaces_imports(nonpublic)
 
     if not "foundation" in namespaces.keys():
         utils.multithread.thread_safe_print(
-            f"'{agda_module}' has no foundation imports. Skipping.")
+            f"'{agda_module}' has no foundation imports.")
         return
 
     new_nonpublic = set(nonpublic)

diff --git a/scripts/generate_main_index_file.py b/scripts/generate_main_index_file.py
@@ -41,7 +41,7 @@ def generate_namespace_entry_list(namespace):
         print(f"WARNING! Duplicate titles in {namespace}:")
         for ec in equal_titles:
             print(
-                f"  Title '{ec[0][0]}': {', '.join(m[1][:m.rfind('.lagda.md')] for m in ec)}")
+                f"  Title '{ec[0][0]}': {', '.join(m[1][:m[1].rfind('.lagda.md')] for m in ec)}")
 
     module_titles_and_mdfiles = sorted(
         zip(module_titles, module_mdfiles), key=lambda tm: (tm[0].casefold(), tm[1]))

diff --git a/scripts/remove_unused_imports.py b/scripts/remove_unused_imports.py
@@ -19,9 +19,13 @@ def process_agda_file(agda_file, agda_options, root, temp_dir):
     agda_module = utils.get_agda_module_name(agda_file, root)
 
     # If no nonpublic imports, skip
-    if not nonpublic:
+    if nonpublic is None:
         utils.multithread.thread_safe_print(
-            f"'{agda_module}' Could not find imports. Skipping.")
+            f"'{agda_module}' Could not find imports.")
+        return
+    elif len(nonpublic) == 0:
+        utils.multithread.thread_safe_print(
+            f"'{agda_module}' No nonpublic imports.")
         return
 
     # Proceed with search for unused imports

diff --git a/src/category-theory/anafunctors.lagda.md b/src/category-theory/anafunctors.lagda.md
@@ -39,7 +39,7 @@ anafunctor-Precat l C D =
       Σ ( (X Y : obj-Precat C) (U : obj-Precat D) (u : F₀ X U) →
           (V : obj-Precat D) (v : F₀ Y V) →
           (f : type-hom-Precat C X Y) → type-hom-Precat D U V)
-        ( λ  F₁ →
+        ( λ F₁ →
           ( ( X : obj-Precat C) → type-trunc-Prop (Σ (obj-Precat D) (F₀ X))) ×
           ( ( ( X : obj-Precat C) (U : obj-Precat D) (u : F₀ X U) →
               F₁ X X U u U u (id-hom-Precat C) ＝ id-hom-Precat D) ×

diff --git a/src/category-theory/isomorphisms-large-precategories.lagda.md b/src/category-theory/isomorphisms-large-precategories.lagda.md
@@ -125,7 +125,7 @@ iso-eq-Large-Precat C X .X refl = id-iso-Large-Precat C
 Let `f : hom x y` and suppose `g g' : hom y x` are both two-sided inverses to
 `f`. It is enough to show that `g = g'` since the equalities are propositions
 (since the hom-types are sets). But we have the following chain of equalities:
-`g = comp g id_y    = comp g (comp f g')    = comp (comp g f) g'    = comp id_x g'    = g'.`
+`g = comp g id_y = comp g (comp f g') = comp (comp g f) g' = comp id_x g' = g'`.
 
 ```agda
 module _

diff --git a/src/commutative-algebra/ideals-commutative-rings.lagda.md b/src/commutative-algebra/ideals-commutative-rings.lagda.md
@@ -13,7 +13,6 @@ open import commutative-algebra.subsets-commutative-rings
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
-open import foundation.subtypes
 open import foundation.universe-levels
 
 open import ring-theory.ideals-rings

diff --git a/src/commutative-algebra/ideals-commutative-semirings.lagda.md b/src/commutative-algebra/ideals-commutative-semirings.lagda.md
@@ -13,11 +13,9 @@ open import commutative-algebra.subsets-commutative-semirings
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
-open import foundation.subtypes
 open import foundation.universe-levels
 
 open import ring-theory.ideals-semirings
-open import ring-theory.subsets-semirings
 ```
 
 </details>

diff --git a/src/commutative-algebra/maximal-ideals-commutative-rings.lagda.md b/src/commutative-algebra/maximal-ideals-commutative-rings.lagda.md
@@ -4,6 +4,14 @@
 module commutative-algebra.maximal-ideals-commutative-rings where
 ```
 
+<details><summary>Imports</summary>
+
+```agda
+
+```
+
+</details>
+
 ## Idea
 
 Maximal ideals in a commutative ring `R` are proper ideals `I` such that any

diff --git a/src/commutative-algebra/nilradical-commutative-rings.lagda.md b/src/commutative-algebra/nilradical-commutative-rings.lagda.md
@@ -7,30 +7,15 @@ module commutative-algebra.nilradical-commutative-rings where
 <details><summary>Imports</summary>
 
 ```agda
-open import commutative-algebra.binomial-theorem-commutative-rings
 open import commutative-algebra.commutative-rings
 open import commutative-algebra.ideals-commutative-rings
-open import commutative-algebra.powers-of-elements-commutative-rings
 open import commutative-algebra.subsets-commutative-rings
-open import commutative-algebra.sums-commutative-rings
 
-open import elementary-number-theory.addition-natural-numbers
-open import elementary-number-theory.binomial-coefficients
-open import elementary-number-theory.distance-natural-numbers
-open import elementary-number-theory.inequality-natural-numbers
-open import elementary-number-theory.natural-numbers
-
-open import foundation.dependent-pair-types
 open import foundation.existential-quantification
 open import foundation.identity-types
-open import foundation.propositional-truncations
-open import foundation.subtypes
 open import foundation.universe-levels
 
 open import ring-theory.nilpotent-elements-rings
-
-open import univalent-combinatorics.coproduct-types
-open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>

diff --git a/src/commutative-algebra/powers-of-elements-commutative-rings.lagda.md b/src/commutative-algebra/powers-of-elements-commutative-rings.lagda.md
@@ -13,7 +13,6 @@ open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.parity-natural-numbers
 
-open import foundation.empty-types
 open import foundation.identity-types
 open import foundation.universe-levels
 

diff --git a/src/commutative-algebra/prime-ideals-commutative-rings.lagda.md b/src/commutative-algebra/prime-ideals-commutative-rings.lagda.md
@@ -16,7 +16,6 @@ open import foundation.disjunction
 open import foundation.propositions
 open import foundation.universe-levels
 
-open import ring-theory.ideals-rings
 open import ring-theory.subsets-rings
 ```
 

diff --git a/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md b/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md
@@ -12,24 +12,16 @@ open import commutative-algebra.commutative-rings
 open import commutative-algebra.ideals-commutative-rings
 open import commutative-algebra.powers-of-elements-commutative-rings
 open import commutative-algebra.subsets-commutative-rings
-open import commutative-algebra.sums-commutative-rings
 
 open import elementary-number-theory.addition-natural-numbers
-open import elementary-number-theory.binomial-coefficients
-open import elementary-number-theory.distance-natural-numbers
-open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.existential-quantification
-open import foundation.identity-types
 open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
-
-open import univalent-combinatorics.coproduct-types
-open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>

diff --git a/src/commutative-algebra/sums-commutative-rings.lagda.md b/src/commutative-algebra/sums-commutative-rings.lagda.md
@@ -180,7 +180,7 @@ module _
   shift-sum-Commutative-Ring = shift-sum-Ring (ring-Commutative-Ring R)
 ```
 
-### Splitting Sums
+### Splitting sums
 
 ```agda
 split-sum-Commutative-Ring :

diff --git a/src/commutative-algebra/sums-commutative-semirings.lagda.md b/src/commutative-algebra/sums-commutative-semirings.lagda.md
@@ -200,7 +200,7 @@ module _
     sum-zero-Semiring (semiring-Commutative-Semiring R)
 ```
 
-### Splitting Sums
+### Splitting sums
 
 ```agda
 split-sum-Commutative-Semiring :

diff --git a/src/elementary-number-theory/bezouts-lemma.lagda.md b/src/elementary-number-theory/bezouts-lemma.lagda.md
@@ -387,7 +387,7 @@ is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) =
     by ap (λ p → add-ℤ (add-ℤ (mul-ℤ (neg-ℤ a) (int-ℕ (succ-ℕ x))) p)
       (add-ℤ (mul-ℤ (int-ℤ-Mod (succ-ℕ x) u) (int-ℕ y))
       (neg-ℤ (mul-ℤ (int-ℕ (succ-ℕ x)) (int-ℕ y)))))
-      (commutative-mul-ℤ  (int-ℕ y) (int-ℕ (succ-ℕ x)))
+      (commutative-mul-ℤ (int-ℕ y) (int-ℕ (succ-ℕ x)))
     ＝ add-ℤ (add-ℤ (mul-ℤ (neg-ℤ a) (int-ℕ (succ-ℕ x)))
        (mul-ℤ (int-ℤ-Mod (succ-ℕ x) u) (int-ℕ y)))
       (add-ℤ (mul-ℤ (int-ℕ (succ-ℕ x)) (int-ℕ y))
@@ -432,7 +432,7 @@ is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) =
       ＝ dist-ℤ (int-ℕ (mul-ℕ (nat-Fin (succ-ℕ x) u) y))
         (int-ℕ (mul-ℕ (abs-ℤ a) (succ-ℕ x)))
         by inv (dist-int-ℕ (mul-ℕ (nat-Fin (succ-ℕ x) u) y)
-          (mul-ℕ (abs-ℤ a)  (succ-ℕ x)))
+          (mul-ℕ (abs-ℤ a) (succ-ℕ x)))
       ＝ dist-ℤ (int-ℕ (mul-ℕ (nat-Fin (succ-ℕ x) u) y))
         (mul-ℤ (int-ℕ (abs-ℤ a)) (int-ℕ (succ-ℕ x)))
         by ap (λ p → dist-ℤ (int-ℕ (mul-ℕ (nat-Fin (succ-ℕ x) u) y)) p)
@@ -792,7 +792,7 @@ remainder-min-dist-succ-x-is-distance x y =
              (int-ℕ (succ-ℕ x))
         by ap (λ H → add-ℤ H (int-ℕ (succ-ℕ x)))
           (distributive-neg-add-ℤ (mul-ℤ (mul-ℤ (int-ℕ q) (int-ℕ t)) (int-ℕ y))
-            (neg-ℤ (mul-ℤ (mul-ℤ (int-ℕ q) (int-ℕ s)) (int-ℕ (succ-ℕ x))))  )
+            (neg-ℤ (mul-ℤ (mul-ℤ (int-ℕ q) (int-ℕ s)) (int-ℕ (succ-ℕ x)))))
         ＝ add-ℤ (add-ℤ (neg-ℤ (mul-ℤ (mul-ℤ (int-ℕ q) (int-ℕ t)) (int-ℕ y)))
            (mul-ℤ (mul-ℤ (int-ℕ q) (int-ℕ s)) (int-ℕ (succ-ℕ x))))
              (int-ℕ (succ-ℕ x))

diff --git a/src/elementary-number-theory/congruence-natural-numbers.lagda.md b/src/elementary-number-theory/congruence-natural-numbers.lagda.md
@@ -160,7 +160,7 @@ is-one-cong-succ-ℕ {k} x H =
 
 ```agda
 scalar-invariant-cong-ℕ :
-  (k x y z : ℕ) → cong-ℕ k x y →  cong-ℕ k (mul-ℕ z x) (mul-ℕ z y)
+  (k x y z : ℕ) → cong-ℕ k x y → cong-ℕ k (mul-ℕ z x) (mul-ℕ z y)
 pr1 (scalar-invariant-cong-ℕ k x y z (pair d p)) = mul-ℕ z d
 pr2 (scalar-invariant-cong-ℕ k x y z (pair d p)) =
   ( associative-mul-ℕ z d k) ∙
@@ -181,7 +181,7 @@ scalar-invariant-cong-ℕ' k x y z H =
 ```agda
 congruence-mul-ℕ :
   (k : ℕ) {x y x' y' : ℕ} →
-  cong-ℕ  k x x' → cong-ℕ k y y' → cong-ℕ k (mul-ℕ x y) (mul-ℕ x' y')
+  cong-ℕ k x x' → cong-ℕ k y y' → cong-ℕ k (mul-ℕ x y) (mul-ℕ x' y')
 congruence-mul-ℕ k {x} {y} {x'} {y'} H K =
   trans-cong-ℕ k (mul-ℕ x y) (mul-ℕ x y') (mul-ℕ x' y')
     ( scalar-invariant-cong-ℕ k y y' x K)

diff --git a/src/elementary-number-theory/divisibility-natural-numbers.lagda.md b/src/elementary-number-theory/divisibility-natural-numbers.lagda.md
@@ -16,7 +16,6 @@ open import elementary-number-theory.natural-numbers
 open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.identity-types
-open import foundation.negation
 open import foundation.propositional-maps
 open import foundation.propositions
 open import foundation.universe-levels

diff --git a/src/elementary-number-theory/finitary-natural-numbers.lagda.md b/src/elementary-number-theory/finitary-natural-numbers.lagda.md
@@ -204,7 +204,7 @@ issec-inv-convert-based-ℕ :
   (k n : ℕ) → convert-based-ℕ (succ-ℕ k) (inv-convert-based-ℕ k n) ＝ n
 issec-inv-convert-based-ℕ k zero-ℕ = is-zero-nat-zero-Fin {k}
 issec-inv-convert-based-ℕ k (succ-ℕ n) =
-  ( convert-based-succ-based-ℕ (succ-ℕ k) (inv-convert-based-ℕ  k n)) ∙
+  ( convert-based-succ-based-ℕ (succ-ℕ k) (inv-convert-based-ℕ k n)) ∙
   ( ap succ-ℕ (issec-inv-convert-based-ℕ k n))
 
 isretr-inv-convert-based-ℕ :

diff --git a/src/elementary-number-theory/goldbach-conjecture.lagda.md b/src/elementary-number-theory/goldbach-conjecture.lagda.md
@@ -8,7 +8,6 @@ module elementary-number-theory.goldbach-conjecture where
 
 ```agda
 open import elementary-number-theory.addition-natural-numbers
-open import elementary-number-theory.divisibility-natural-numbers
 open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.parity-natural-numbers
@@ -22,7 +21,7 @@ open import foundation.universe-levels
 
 </details>
 
-# The Goldbach Conjecture
+## Conjecture
 
 ```agda
 Goldbach-conjecture : UU lzero