Merge branch 'master' into lower-upper-neg

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

@@ -22,8 +22,10 @@ open import foundation.universe-levels
 
 ## Idea
 
-Given a [category](category-theory.categories.md) `C`, an object `c`, and a
-[functor](category-theory.functors-categories.md) `F` from `C` to the
+The
+{{#concept "Yoneda lemma" Disambiguation="for set-level categories" WD="Yoneda lemma" WDID=Q320577 Agda=lemma-yoneda-Category}}
+states that, given a [category](category-theory.categories.md) `C`, an object
+`c`, and a [functor](category-theory.functors-categories.md) `F` from `C` to the
 [category of sets](foundation.category-of-sets.md)
 
 ```text
@@ -40,9 +42,9 @@ from the functor
   Nat(Hom(c , -) , F) ≃ F c
 ```
 
-More precisely, the **Yoneda lemma** asserts that the map from the type of
-natural transformations to the type `F c` defined by evaluating the component of
-the natural transformation at the object `c` at the identity arrow on `c` is an
+More precisely, the Yoneda lemma asserts that the map from the type of natural
+transformations to the type `F c` defined by evaluating the component of the
+natural transformation at the object `c` at the identity arrow on `c` is an
 equivalence.
 
 ## Theorem

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

@@ -29,9 +29,11 @@ open import foundation.universe-levels
 
 ## Idea
 
-Given a [precategory](category-theory.precategories.md) `C`, an object `c`, and
-a [functor](category-theory.functors-precategories.md) `F` from `C` to the
-[category of sets](foundation.category-of-sets.md)
+The
+{{#concept "Yoneda lemma" Disambiguation="for set-level precategories" WD="Yoneda lemma" WDID=Q320577 Agda=lemma-yoneda-Precategory}}
+states that, given a [precategory](category-theory.precategories.md) `C`, an
+object `c`, and a [functor](category-theory.functors-precategories.md) `F` from
+`C` to the [category of sets](foundation.category-of-sets.md)
 
 ```text
   F : C → Set,
@@ -47,9 +49,9 @@ from the functor
   Nat(Hom(c , -) , F) ≃ F c
 ```
 
-More precisely, the **Yoneda lemma** asserts that the map from the type of
-natural transformations to the type `F c` defined by evaluating the component of
-the natural transformation at the object `c` at the identity arrow on `c` is an
+More precisely, the Yoneda lemma asserts that the map from the type of natural
+transformations to the type `F c` defined by evaluating the component of the
+natural transformation at the object `c` at the identity arrow on `c` is an
 equivalence.
 
 ## Theorem

src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md

@@ -39,8 +39,8 @@ The **binomial theorem** in commutative rings asserts that for any two elements
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
-The binomial theorem is the 44th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+The binomial theorem is the [44th](literature.100-theorems.md#44) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md

@@ -39,8 +39,8 @@ we have
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
-The binomial theorem is the 44th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+The binomial theorem is the [44th](literature.100-theorems.md#44) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

src/elementary-number-theory/bezouts-lemma-integers.lagda.md

@@ -38,8 +38,8 @@ open import foundation.unit-type
 
 </details>
 
-Bézout's Lemma is the 60th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+Bézout's Lemma is the [60th](literature.100-theorems.md#60) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}. It was
 originally added to agda-unimath by [Bryan Lu](https://blu-bird.github.io).
 

src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md

@@ -61,8 +61,8 @@ predicate `P : ℕ → UU lzero` given by
 is decidable, because `P z ⇔ [y]_x | [z]_x` in `ℤ/x`. The least positive `z`
 such that `P z` holds is `gcd x y`.
 
-Bézout's Lemma is the 60th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+Bézout's Lemma is the [60th](literature.100-theorems.md#60) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}. It was
 originally added to agda-unimath by [Bryan Lu](https://blu-bird.github.io).
 

src/elementary-number-theory/binomial-theorem-integers.lagda.md

@@ -36,8 +36,8 @@ The binomial theorem for the integers asserts that for any two integers `x` and
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
-The binomial theorem is the 44th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+The binomial theorem is the [44th](literature.100-theorems.md#44) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

src/elementary-number-theory/binomial-theorem-natural-numbers.lagda.md

@@ -35,8 +35,8 @@ numbers `x` and `y` and any natural number `n`, we have
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
-The binomial theorem is the 44th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+The binomial theorem is the [44th](literature.100-theorems.md#44) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

src/elementary-number-theory/falling-factorials.lagda.md

@@ -40,7 +40,7 @@ Fin-falling-factorial-ℕ :
   (n m : ℕ) → Fin (falling-factorial-ℕ n m) ≃ (Fin m ↪ Fin n)
 Fin-falling-factorial-ℕ zero-ℕ zero-ℕ =
   equiv-is-contr
-    ( is-contr-Fin-one-ℕ)
+    ( is-contr-Fin-1)
     ( is-contr-equiv
       ( is-emb id)
       ( left-unit-law-Σ-is-contr
@@ -52,7 +52,7 @@ Fin-falling-factorial-ℕ zero-ℕ (succ-ℕ m) =
   equiv-is-empty id (λ f → map-emb f (inr star))
 Fin-falling-factorial-ℕ (succ-ℕ n) zero-ℕ =
   equiv-is-contr
-    ( is-contr-Fin-one-ℕ)
+    ( is-contr-Fin-1)
     ( is-contr-equiv
       ( is-emb ex-falso)
       ( left-unit-law-Σ-is-contr

src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md

@@ -75,8 +75,9 @@ in several ways:
 Note that the [univalence axiom](foundation-core.univalence.md) is neccessary to
 prove the second uniqueness property of prime factorizations.
 
-The fundamental theorem of arithmetic is the 80th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+The fundamental theorem of arithmetic is the
+[80th](literature.100-theorems.md#80) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md

@@ -42,8 +42,9 @@ The greatest common divisor of two natural numbers `x` and `y` is a number
 `gcd x y` such that any natural number `d : ℕ` is a common divisor of `x` and
 `y` if and only if it is a divisor of `gcd x y`.
 
-The algorithm defining the greatest common divisor is the 69th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+The algorithm defining the greatest common divisor is the
+[69th](literature.100-theorems.md#69) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definition

src/elementary-number-theory/infinitude-of-primes.lagda.md

@@ -42,10 +42,11 @@ the
 that there are infinitely many
 [primes](elementary-number-theory.prime-numbers.md). Consequently we obtain the
 function that returns for each `n` the `n`-th prime, and we obtain the function
-that counts the number of primes below a number `n`.
+that counts the number of primes below a number `n`. This result is known as
+{{#concept "Euclid's theorem" WD="Euclid's theorem" WDID=Q1506253 Agda=infinitude-of-primes-ℕ}}
 
-The infinitude of primes is the 11th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+The infinitude of primes is the [11th](literature.100-theorems.md#11) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definition
@@ -188,3 +189,8 @@ prime-counting-ℕ (succ-ℕ n) =
 ## References
 
 {{#bibliography}}
+
+## External links
+
+- [Euclid's theorem](https://en.wikipedia.org/wiki/Euclid%27s_theorem) on
+  Wikipedia

src/elementary-number-theory/natural-numbers.lagda.md

@@ -83,8 +83,9 @@ is-not-one-ℕ' n = ¬ (is-one-ℕ' n)
 
 ### The induction principle of ℕ
 
-The induction principle of the natural numbers is the 74th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+The induction principle of the natural numbers is the
+[74th](literature.100-theorems.md#74) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ```agda

src/elementary-number-theory/rational-numbers.lagda.md

@@ -206,8 +206,9 @@ retract-integer-fraction-ℚ =
 
 ### The rationals are countable
 
-The denumerability of the rational numbers is the third theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+The denumerability of the rational numbers is the
+[third](literature.100-theorems.md#3) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ```agda

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

@@ -929,11 +929,11 @@ is-finite-Q8 = unit-trunc-Prop count-Q8
 Q8-Finite-Type : Finite-Type lzero
 Q8-Finite-Type = pair Q8 is-finite-Q8
 
-has-cardinality-eight-Q8 : has-cardinality 8 Q8
+has-cardinality-eight-Q8 : has-cardinality-ℕ 8 Q8
 has-cardinality-eight-Q8 = unit-trunc-Prop equiv-count-Q8
 
-Q8-UU-Fin-8 : UU-Fin lzero 8
-Q8-UU-Fin-8 = pair Q8 has-cardinality-eight-Q8
+Q8-Type-With-Cardinality-ℕ : Type-With-Cardinality-ℕ lzero 8
+Q8-Type-With-Cardinality-ℕ = pair Q8 has-cardinality-eight-Q8
 
 has-finite-cardinality-Q8 : has-finite-cardinality Q8
 has-finite-cardinality-Q8 = pair 8 has-cardinality-eight-Q8

src/finite-group-theory/alternating-concrete-groups.lagda.md

@@ -35,7 +35,7 @@ module _
   alternating-Concrete-Group : Concrete-Group (lsuc (lsuc lzero))
   alternating-Concrete-Group =
     concrete-group-kernel-hom-Concrete-Group
-      ( UU-Fin-Group lzero n)
-      ( UU-Fin-Group (lsuc lzero) 2)
+      ( Type-With-Cardinality-ℕ-Concrete-Group lzero n)
+      ( Type-With-Cardinality-ℕ-Concrete-Group (lsuc lzero) 2)
       ( cartier-delooping-sign n)
 ```

src/finite-group-theory/alternating-groups.lagda.md

@@ -30,11 +30,11 @@ The alternating group on a finite set `X` is the group of even permutations of
 
 ```agda
 module _
-  {l} (n : ℕ) (X : UU-Fin l n)
+  {l} (n : ℕ) (X : Type-With-Cardinality-ℕ l n)
   where
   alternating-Group : Group l
   alternating-Group = group-kernel-hom-Group
-    ( symmetric-Group (set-UU-Fin n X))
+    ( symmetric-Group (set-Type-With-Cardinality-ℕ n X))
     ( symmetric-Group (Fin-Set 2))
     ( sign-homomorphism n X)
 ```

src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md

@@ -128,7 +128,10 @@ module _
         (n +ℕ 2 , (compute-raise l (Fin (n +ℕ 2)))) (star))
 
   cartier-delooping-sign :
-    (n : ℕ) → hom-Concrete-Group (UU-Fin-Group l n) (UU-Fin-Group (lsuc l) 2)
+    (n : ℕ) →
+    hom-Concrete-Group
+      ( Type-With-Cardinality-ℕ-Concrete-Group l n)
+      ( Type-With-Cardinality-ℕ-Concrete-Group (lsuc l) 2)
   cartier-delooping-sign =
     quotient-delooping-sign
       ( orientation-Complete-Undirected-Graph)
@@ -146,29 +149,29 @@ module _
       ( comp-hom-Group
         ( symmetric-Group (raise-Fin-Set l (n +ℕ 2)))
         ( loop-group-Set (raise-Fin-Set l (n +ℕ 2)))
-        ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
+        ( Type-With-Cardinality-ℕ-Group (lsuc l) 2)
         ( comp-hom-Group
           ( loop-group-Set (raise-Fin-Set l (n +ℕ 2)))
-          ( group-Concrete-Group (UU-Fin-Group l (n +ℕ 2)))
-          ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
+          ( Type-With-Cardinality-ℕ-Group l (n +ℕ 2))
+          ( Type-With-Cardinality-ℕ-Group (lsuc l) 2)
           ( hom-group-hom-Concrete-Group
-            ( UU-Fin-Group l (n +ℕ 2))
-            ( UU-Fin-Group (lsuc l) 2)
+            ( Type-With-Cardinality-ℕ-Concrete-Group l (n +ℕ 2))
+            ( Type-With-Cardinality-ℕ-Concrete-Group (lsuc l) 2)
             ( cartier-delooping-sign (n +ℕ 2)))
           ( hom-inv-iso-Group
-            ( group-Concrete-Group (UU-Fin-Group l (n +ℕ 2)))
+            ( Type-With-Cardinality-ℕ-Group l (n +ℕ 2))
             ( loop-group-Set (raise-Fin-Set l (n +ℕ 2)))
-            ( iso-loop-group-fin-UU-Fin-Group l (n +ℕ 2))))
+            ( iso-loop-group-fin-Type-With-Cardinality-ℕ-Group l (n +ℕ 2))))
         ( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l (n +ℕ 2))))
       ( comp-hom-Group
         ( symmetric-Group (raise-Fin-Set l (n +ℕ 2)))
         ( symmetric-Group (Fin-Set (n +ℕ 2)))
-        ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
+        ( Type-With-Cardinality-ℕ-Group (lsuc l) 2)
         ( comp-hom-Group
           ( symmetric-Group (Fin-Set (n +ℕ 2)))
           ( symmetric-Group (Fin-Set 2))
-          ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
-          ( symmetric-abstract-UU-fin-group-quotient-hom
+          ( Type-With-Cardinality-ℕ-Group (lsuc l) 2)
+          ( symmetric-abstract-type-with-cardinality-ℕ-group-quotient-hom
             ( orientation-Complete-Undirected-Graph)
             ( even-difference-orientation-Complete-Undirected-Graph)
             ( λ n _ →

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

@@ -37,10 +37,10 @@ equiv-face-cube :
       ( map-axis-equiv-cube (succ-ℕ k) X Y e d a))
 equiv-face-cube k X Y e d a =
   pair
-    ( equiv-complement-element-UU-Fin k
-      ( pair (dim-cube-UU-Fin (succ-ℕ k) X) d)
+    ( equiv-complement-element-Type-With-Cardinality-ℕ k
+      ( pair (dim-cube-Type-With-Cardinality-ℕ (succ-ℕ k) X) d)
       ( pair
-        ( dim-cube-UU-Fin (succ-ℕ k) Y)
+        ( dim-cube-Type-With-Cardinality-ℕ (succ-ℕ k) Y)
         ( map-dim-equiv-cube (succ-ℕ k) X Y e d))
       ( dim-equiv-cube (succ-ℕ k) X Y e)
       ( refl))
@@ -52,24 +52,24 @@ equiv-face-cube k X Y e d a =
             ( dim-equiv-cube (succ-ℕ k) X Y e)
             ( pair d
               ( λ z →
-                has-decidable-equality-has-cardinality
+                has-decidable-equality-has-cardinality-ℕ
                   ( succ-ℕ k)
                   ( has-cardinality-dim-cube (succ-ℕ k) X)
                   ( d)
                   ( z)))
             ( pair
               ( map-dim-equiv-cube (succ-ℕ k) X Y e d)
               ( λ z →
-                has-decidable-equality-has-cardinality
+                has-decidable-equality-has-cardinality-ℕ
                   ( succ-ℕ k)
                   ( has-cardinality-dim-cube (succ-ℕ k) Y)
                   ( map-dim-equiv-cube (succ-ℕ k) X Y e d)
                   ( z)))
             ( refl)
             ( d')))) ∘e
       ( axis-equiv-cube (succ-ℕ k) X Y e
-        ( inclusion-complement-element-UU-Fin k
-          ( pair (dim-cube-UU-Fin (succ-ℕ k) X) d) d')))
+        ( inclusion-complement-element-Type-With-Cardinality-ℕ k
+          ( pair (dim-cube-Type-With-Cardinality-ℕ (succ-ℕ k) X) d) d')))
 
 cube-with-labeled-faces :
   (k : ℕ) → UU (lsuc lzero)