Refactor files about identity types and homotopies (#1014)

The following files were significantly cleaned up: - `foundation.path-algebra` The following files were created: - `foundation.action-on-higher-identifications-functions` - `foundation.whiskering-higher-homotopies` - `foundation.whiskering-identifications` The following other actions were performed: - Adding detailed informal explanations to many entries affected by this pull request. - Replace `whisk` with `whisker` throughout the library. - Making the order of arguments uniform for various operations on commuting squares and triangles of identifications. - Fixing names so that operator names go before the entity that they act on: * `htpy-left-whisker` to `htpy-left-whisker` * `coherence-square-identifications-horizontal-inv` to `horizontal-inv-coherence-square-identifications` * `coherence-square-identifications-left-paste` to `left-concat-identification-coherence-square-identification`, and variants - Replace `ap (ap f)` with `ap² f` throughout the library. I also renamed the various `nat-sq`-entries about `ap²`. - Moving the entries about squares of identifications from `path-algebra` to `commuting-squares-of-identifications`. - There were duplicate entries that did the same pasting lemmas of commuting squares of identifications, spread out over several files including `commuting-squares-of-identifications` and `path-algebra`. These separate formalization attempts have been unified. - Removing "iterated inverse laws" from `path-algebra` since they were duplicate entries and they were not actually iterated. - Rename `ap-concat-eq` to `map-coherence-triangle-identifications`, change the order of its arguments to match with `coherence-triangle-identifications`, and move it to `commuting-triangles-of-identifications`. - Rename `coherence-square-identifications-ap` to `map-coherence-square-identifications`. - Remove entries `inv-htpy-left-whisk-inv-htpy` and `inv-htpy-right-whisk-inv-htpy`. - Rename `ap-left-whisk-htpy` to `left-whisker-htpy²`, and `ap-right-whisk-htpy` to `right-whisker-htpy²` and move them to `whiskering-higher-homotopies`. - Correcting a statement that `refl-htpy` is a unit element on the homotopy side for whiskering. Instead, it is an absorbing element. --------- Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
UniMath · Feb 6, 2024 · 9b1707d · 9b1707d
1 parent ae02da9
commit 9b1707d
Show file tree

Hide file tree

Showing 271 changed files with 7,614 additions and 3,838 deletions.
diff --git a/FILE-CONVENTIONS.md b/FILE-CONVENTIONS.md
@@ -59,10 +59,10 @@ open import ... public
 
 ### Imports block
 
-After the module declaration, include an Agda code block of all non-public
-module imports starting with `<details><summary>Imports</summary>` and ending
-with `</details>`. This block should only contain module imports and there
-should have no further import statements after it. In the rendered markdown, the
+After the module declaration, include an Agda code block of all nonpublic module
+imports starting with `<details><summary>Imports</summary>` and ending with
+`</details>`. This block should only contain module imports and there should
+have no further import statements after it. In the rendered markdown, the
 contents of this block will be hidden by default, but can be revealed by
 clicking on _Imports_.
 

diff --git a/MIXFIX-OPERATORS.md b/MIXFIX-OPERATORS.md
@@ -18,7 +18,7 @@ accepted notation for widely used operators.
 Mixfix operators can each be assigned a
 [precedence level](https://agda.readthedocs.io/en/latest/language/mixfix-operators.html#precedence).
 This can in principle be any signed fractional value, although we prefer them to
-be non-negative integral values. The higher this value is, the higher precedence
+be nonnegative integral values. The higher this value is, the higher precedence
 the operator has, meaning it is evaluated before operators with lower
 precedence. By default in Agda, an operator is assigned a precedence level of
 `20`.
@@ -47,15 +47,15 @@ By default, an operator does not associate to either side.
 
 We divide the different operators into broad classes, each assigned a range of
 possible precedence levels. In broad terms, we discern between _parametric_ and
-_non-parametric_ operators. The general rule is that non-parametric operator has
+_nonparametric_ operators. The general rule is that nonparametric operator has
 higher precedence than parametric operators. Parametric operators are operators
 that take a universe level as one of their arguments. We consider an operator to
 be parametric even if it only takes a universe level as an implicit argument.
 Examples are the
 [cartesian product type former`_×_`](foundation-core.cartesian-product-types.md),
 the [identity type former `_＝_`](foundation-core.identity-types.md), and the
 [pairing operator `_,_`](foundation.dependent-pair-types.md). Examples of
-non-parametric operators are
+nonparametric operators are
 [difference of integers `_-ℤ_`](elementary-number-theory.difference-integers.md),
 [strict inequality on natural numbers `_<-ℕ_`](elementary-number-theory.strict-inequality-natural-numbers.md),
 and
@@ -129,7 +129,7 @@ Below, we outline a list of general rules when assigning associativities.
   to right. For instance, the expression `1 - 2 - 3` is computed as
   `(1 - 2) - 3 = -1 - 3 = -4`, hence should be _left associative_. This applies
   to addition, subtraction, multiplication, and division. Note that for
-  non-parametric exponentiation, we compute from right to left. I.e. `2 ^ 3 ^ 4`
+  nonparametric exponentiation, we compute from right to left. I.e. `2 ^ 3 ^ 4`
   should compute as `2 ^ (3 ^ 4)`. Hence it will usually be _right associative_.
 
 - **Arithmetic type formers** such as
@@ -165,7 +165,7 @@ Below, we outline a list of general rules when assigning associativities.
 
 | Precedence level | Operators                                                                                                                                                                                   |
 | ---------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
-| 50               | Unary non-parametric operators. This class is currently empty                                                                                                                               |
+| 50               | Unary nonparametric operators. This class is currently empty                                                                                                                                |
 | 45               | Exponentiative arithmetic operators                                                                                                                                                         |
 | 40               | Multiplicative arithmetic operators                                                                                                                                                         |
 | 36               | Subtractive arithmetic operators                                                                                                                                                            |

diff --git a/book.toml b/book.toml
@@ -26,7 +26,7 @@ assets_version = "1.2.0" # DO NOT EDIT: Managed by `mdbook-catppuccin install`
 
 [preprocessor.git-metadata]
 command = "python3 ./scripts/preprocessor_git_metadata.py"
-# Disable by default - it takes a non-trivial amount of time
+# Disable by default - it takes a nontrivial amount of time
 # Can be overriden by running
 # `export MDBOOK_PREPROCESSOR__GIT_METADATA__ENABLE=true` in your shell
 enable = false

diff --git a/flake.nix b/flake.nix
@@ -38,7 +38,7 @@
             # We can reference the directory since we're using flakes,
             # which copies the version-tracked files into the nix store
             # before evaluation, # so we don't run into the issue with
-            # non-reproducible source paths as outlined here:
+            # nonreproducible source paths as outlined here:
             # https://nix.dev/recipes/best-practices#reproducible-source-paths
             src = ./.;
 

diff --git a/scripts/even_indentation_conventions.py b/scripts/even_indentation_conventions.py
@@ -67,6 +67,6 @@ def is_even_indentation(line):
         print(*map(lambda kv: f'  {kv[0]}: {kv[1]} lines',
                    sorted(offender_files.items(), key=lambda kv: kv[1])), sep='\n')
         print(
-            f'\nTotal number of lines in library unevenly indented: {sum(offender_files.values())}.\n\nUneven indentation means that there is code indented by a non-multiple of the base indentation (2 spaces). If you haven\'t already, we suggest you set up your environment to more easily spot uneven indentation. For instance using VSCode\'s indent-rainbow extension.')
+            f'\nTotal number of lines in library unevenly indented: {sum(offender_files.values())}.\n\nUneven indentation means that there is code indented by a nonmultiple of the base indentation (2 spaces). If you haven\'t already, we suggest you set up your environment to more easily spot uneven indentation. For instance using VSCode\'s indent-rainbow extension.')
 
     sys.exit(status)
diff --git a/src/category-theory/adjunctions-large-precategories.lagda.md b/src/category-theory/adjunctions-large-precategories.lagda.md
@@ -160,7 +160,7 @@ module _
       ( map-inv-equiv-is-adjoint-pair-Large-Precategory H X2 Y2)
   naturality-inv-equiv-is-adjoint-pair-Large-Precategory
     H {X1 = X1} {X2} {Y1} {Y2} f g =
-    coherence-square-inv-horizontal
+    coherence-square-maps-inv-equiv-horizontal
       ( equiv-is-adjoint-pair-Large-Precategory H X1 Y1)
       ( λ h →
         comp-hom-Large-Precategory D

diff --git a/src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md b/src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md
@@ -52,7 +52,7 @@ module _
 
 ### Associative composition operations in binary families of sets
 
-We give a slightly non-standard definition of associativity, requiring an
+We give a slightly nonstandard definition of associativity, requiring an
 associativity witness in each direction. This is of course redundant as `inv` is
 a [fibered involution](foundation.fibered-involutions.md) on
 [identity types](foundation-core.identity-types.md). However, by recording both

diff --git a/src/category-theory/nonunital-precategories.lagda.md b/src/category-theory/nonunital-precategories.lagda.md
@@ -196,7 +196,7 @@ module _
 
 ## Properties
 
-### If the objects of a nonunital precategory are `k`-truncated for non-negative `k`, the total hom-type is `k`-truncated
+### If the objects of a nonunital precategory are `k`-truncated for nonnegative `k`, the total hom-type is `k`-truncated
 
 ```agda
 module _

diff --git a/src/category-theory/precategories.lagda.md b/src/category-theory/precategories.lagda.md
@@ -248,7 +248,7 @@ module _
 
 ## Properties
 
-### If the objects of a precategory are `k`-truncated for non-negative `k`, the total hom-type is `k`-truncated
+### If the objects of a precategory are `k`-truncated for nonnegative `k`, the total hom-type is `k`-truncated
 
 ```agda
 module _

diff --git a/src/category-theory/set-magmoids.lagda.md b/src/category-theory/set-magmoids.lagda.md
@@ -189,7 +189,7 @@ module _
 
 ## Properties
 
-### If the objects of a set-magmoid are `k`-truncated for non-negative `k`, the total hom-type is `k`-truncated
+### If the objects of a set-magmoid are `k`-truncated for nonnegative `k`, the total hom-type is `k`-truncated
 
 ```agda
 module _

diff --git a/src/category-theory/simplex-category.lagda.md b/src/category-theory/simplex-category.lagda.md
@@ -162,6 +162,6 @@ This remains to be formalized.
 
 This remains to be formalized.
 
-### There is a unique non-trivial involution on the simplex category
+### There is a unique nontrivial involution on the simplex category
 
 This remains to be formalized.
diff --git a/src/category-theory/slice-precategories.lagda.md b/src/category-theory/slice-precategories.lagda.md
@@ -412,10 +412,8 @@ module _
       map-inv-pullback-product-Slice-Precategory) ~ id
   is-section-map-inv-pullback-product-Slice-Precategory
     ((Z , .(comp-hom-Precategory C f h₁)) , (h₁ , refl) , (h₂ , β₂) , q) =
-    eq-pair-Σ
-      ( refl)
-      ( eq-pair-Σ
-        ( refl)
+    eq-pair-eq-fiber
+      ( eq-pair-eq-fiber
         ( eq-type-subtype
           ( λ _ →
             is-product-prop-Precategory
@@ -432,12 +430,9 @@ module _
       map-pullback-product-Slice-Precategory) ~ id
   is-retraction-map-inv-pullback-product-Slice-Precategory
     ( W , p₁ , p₂ , α , q) =
-    eq-pair-Σ
-      ( refl)
-      ( eq-pair-Σ
-          ( refl)
-          ( eq-pair-Σ
-              ( refl)
+    eq-pair-eq-fiber
+      ( eq-pair-eq-fiber
+          ( eq-pair-eq-fiber
               ( eq-type-subtype
                   (λ _ → is-pullback-prop-Precategory C A X Y f g _ _ _ α)
                   ( refl))))

diff --git a/src/commutative-algebra/euclidean-domains.lagda.md b/src/commutative-algebra/euclidean-domains.lagda.md
@@ -55,7 +55,7 @@ open import ring-theory.semirings
 A **Euclidean domain** is an
 [integral domain](commutative-algebra.integral-domains.md) `R` that has a
 **Euclidean valuation**, i.e., a function `v : R → ℕ` such that for every
-`x y : R`, if `y` is non-zero then there are `q r : R` with `x = q y + r` and
+`x y : R`, if `y` is nonzero then there are `q r : R` with `x = q y + r` and
 `v r < v y`.
 
 ## Definition

diff --git a/src/commutative-algebra/local-commutative-rings.lagda.md b/src/commutative-algebra/local-commutative-rings.lagda.md
@@ -23,10 +23,9 @@ open import ring-theory.rings
 ## Idea
 
 A **local ring** is a ring such that whenever a sum of elements is invertible,
-then one of its summands is invertible. This implies that the non-invertible
+then one of its summands is invertible. This implies that the noninvertible
 elements form an ideal. However, the law of excluded middle is needed to show
-that any ring of which the non-invertible elements form an ideal is a local
-ring.
+that any ring of which the noninvertible elements form an ideal is a local ring.
 
 ## Definition
 

diff --git a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md b/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md
@@ -282,7 +282,7 @@ If `x = 0`, then we can simply argue in `ℤ`. Otherwise, if `[y] | [z]` in
 `x > u ≥ 0`. Therefore, there exists some integer `a ≥ 0` such that
 `ax = uy - z`, or `ax = z - uy`. In the first case, we can extract the distance
 condition we desire. In the other case, we have that `ax + uy = z`. This can be
-written as `(a + y)x + (u - x)y = z`, so that the second term is non-positive.
+written as `(a + y)x + (u - x)y = z`, so that the second term is nonpositive.
 Then, in this case, we again can extract the distance condition we desire.
 
 ```agda

diff --git a/src/elementary-number-theory/equality-integers.lagda.md b/src/elementary-number-theory/equality-integers.lagda.md
@@ -123,7 +123,7 @@ contraction-total-Eq-ℤ (inl x) (pair (inl y) e) =
     ( ap inl (eq-Eq-ℕ x y e))
     ( eq-is-prop (is-prop-Eq-ℕ x y))
 contraction-total-Eq-ℤ (inr (inl star)) (pair (inr (inl star)) e) =
-  eq-pair-Σ refl (eq-is-prop is-prop-unit)
+  eq-pair-eq-fiber (eq-is-prop is-prop-unit)
 contraction-total-Eq-ℤ (inr (inr x)) (pair (inr (inr y)) e) =
   eq-pair-Σ
     ( ap (inr ∘ inr) (eq-Eq-ℕ x y e))

diff --git a/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md b/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md
@@ -176,7 +176,7 @@ pr1 (is-nontrivial-divisor-diagonal-ℕ n H) = H
 pr2 (is-nontrivial-divisor-diagonal-ℕ n H) = refl-div-ℕ n
 ```
 
-If `l` is a prime decomposition of `n`, then `l` is a list of non-trivial
+If `l` is a prime decomposition of `n`, then `l` is a list of nontrivial
 divisors of `n`.
 
 ```agda
@@ -701,11 +701,11 @@ pr1 (prime-decomposition-fundamental-theorem-arithmetic-list-ℕ x H) =
 pr2 (prime-decomposition-fundamental-theorem-arithmetic-list-ℕ x H) =
   is-prime-decomposition-list-fundamental-theorem-arithmetic-ℕ x H
 
-le-one-is-non-empty-prime-decomposition-list-ℕ :
+le-one-is-nonempty-prime-decomposition-list-ℕ :
   (x : ℕ) (H : leq-ℕ 1 x) (y : ℕ) (l : list ℕ) →
   is-prime-decomposition-list-ℕ x (cons y l) →
   le-ℕ 1 x
-le-one-is-non-empty-prime-decomposition-list-ℕ x H y l D =
+le-one-is-nonempty-prime-decomposition-list-ℕ x H y l D =
   concatenate-le-leq-ℕ
     {x = 1}
     {y = y}
@@ -861,7 +861,7 @@ eq-prime-decomposition-list-ℕ x H (cons y l) nil I J =
     ( contradiction-le-ℕ
       ( 1)
       ( x)
-      ( le-one-is-non-empty-prime-decomposition-list-ℕ x H y l I)
+      ( le-one-is-nonempty-prime-decomposition-list-ℕ x H y l I)
       ( leq-eq-ℕ
         ( x)
         ( 1)
@@ -871,7 +871,7 @@ eq-prime-decomposition-list-ℕ x H nil (cons y l) I J =
     ( contradiction-le-ℕ
       ( 1)
       ( x)
-      ( le-one-is-non-empty-prime-decomposition-list-ℕ x H y l J)
+      ( le-one-is-nonempty-prime-decomposition-list-ℕ x H y l J)
       ( leq-eq-ℕ
         ( x)
         ( 1)

diff --git a/src/elementary-number-theory/sums-of-natural-numbers.lagda.md b/src/elementary-number-theory/sums-of-natural-numbers.lagda.md
@@ -22,7 +22,7 @@ open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.unit-type
 open import foundation.universe-levels
-open import foundation.whiskering-homotopies
+open import foundation.whiskering-homotopies-composition
 
 open import lists.lists
 

diff --git a/src/elementary-number-theory/universal-property-integers.lagda.md b/src/elementary-number-theory/universal-property-integers.lagda.md
@@ -216,7 +216,7 @@ abstract
 
 ### The universal property of the integers
 
-The non-dependent universal property of the integers is a special case of the
+The nondependent universal property of the integers is a special case of the
 dependent universal property applied to constant type families.
 
 ```agda

diff --git a/src/elementary-number-theory/universal-property-natural-numbers.lagda.md b/src/elementary-number-theory/universal-property-natural-numbers.lagda.md
@@ -22,6 +22,7 @@ open import foundation.identity-types
 open import foundation.structure-identity-principle
 open import foundation.torsorial-type-families
 open import foundation.universe-levels
+open import foundation.whiskering-identifications-concatenation
 ```
 
 </details>
@@ -112,7 +113,9 @@ module _
       ( pr2 (pr2 center-structure-preserving-map-ℕ) n ∙ ap f (α n)) ＝
       ( α (succ-ℕ n) ∙ pr2 (pr2 h) n)
     γ n = ( ( inv right-unit) ∙
-            ( ap (λ q → (ap f (α n) ∙ q)) (inv (left-inv (pr2 (pr2 h) n))))) ∙
+            ( left-whisker-concat
+              ( ap f (α n))
+              ( inv (left-inv (pr2 (pr2 h) n))))) ∙
           ( inv
             ( assoc (ap f (α n)) (inv (pr2 (pr2 h) n)) (pr2 (pr2 h) n)))