Page for 1000+ theorems (#1324)

Related to #1322 and #1214.

Author: fredrik-bakke

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/elementary-number-theory/infinitude-of-primes.lagda.md

@@ -42,7 +42,8 @@ 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](literature.100-theorems.md#11) theorem on
 [Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
@@ -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/foundation-core/equivalence-relations.lagda.md

@@ -9,15 +9,19 @@ module foundation-core.equivalence-relations where
 ```agda
 open import foundation.binary-relations
 open import foundation.dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
 open import foundation.inhabited-subtypes
 open import foundation.logical-equivalences
 open import foundation.propositional-truncations
+open import foundation.subtype-identity-principle
 open import foundation.unit-type
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
 open import foundation-core.equivalences
+open import foundation-core.identity-types
 open import foundation-core.propositions
+open import foundation-core.torsorial-type-families
 ```
 
 </details>
@@ -200,3 +204,63 @@ pr1 (pr2 (pr2 (raise-indiscrete-equivalence-relation l A))) _ _ _ = raise-star
 pr2 (pr2 (pr2 (raise-indiscrete-equivalence-relation l A))) _ _ _ _ _ =
   raise-star
 ```
+
+### Characterization of equality in the type of equivalence relations
+
+```agda
+relate-same-elements-equivalence-relation :
+  {l1 l2 l3 : Level} {A : UU l1} →
+  equivalence-relation l2 A → equivalence-relation l3 A → UU (l1 ⊔ l2 ⊔ l3)
+relate-same-elements-equivalence-relation R S =
+  relates-same-elements-Relation-Prop
+    ( prop-equivalence-relation R)
+    ( prop-equivalence-relation S)
+
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  refl-relate-same-elements-equivalence-relation :
+    relate-same-elements-equivalence-relation R R
+  refl-relate-same-elements-equivalence-relation =
+    refl-relates-same-elements-Relation-Prop (prop-equivalence-relation R)
+
+  is-torsorial-relate-same-elements-equivalence-relation :
+    is-torsorial (relate-same-elements-equivalence-relation R)
+  is-torsorial-relate-same-elements-equivalence-relation =
+    is-torsorial-Eq-subtype
+      ( is-torsorial-relates-same-elements-Relation-Prop
+        ( prop-equivalence-relation R))
+      ( is-prop-is-equivalence-relation)
+      ( prop-equivalence-relation R)
+      ( refl-relate-same-elements-equivalence-relation)
+      ( is-equivalence-relation-prop-equivalence-relation R)
+
+  relate-same-elements-eq-equivalence-relation :
+    (S : equivalence-relation l2 A) →
+    (R ＝ S) → relate-same-elements-equivalence-relation R S
+  relate-same-elements-eq-equivalence-relation .R refl =
+    refl-relate-same-elements-equivalence-relation
+
+  is-equiv-relate-same-elements-eq-equivalence-relation :
+    (S : equivalence-relation l2 A) →
+    is-equiv (relate-same-elements-eq-equivalence-relation S)
+  is-equiv-relate-same-elements-eq-equivalence-relation =
+    fundamental-theorem-id
+      is-torsorial-relate-same-elements-equivalence-relation
+      relate-same-elements-eq-equivalence-relation
+
+  extensionality-equivalence-relation :
+    (S : equivalence-relation l2 A) →
+    (R ＝ S) ≃ relate-same-elements-equivalence-relation R S
+  pr1 (extensionality-equivalence-relation S) =
+    relate-same-elements-eq-equivalence-relation S
+  pr2 (extensionality-equivalence-relation S) =
+    is-equiv-relate-same-elements-eq-equivalence-relation S
+
+  eq-relate-same-elements-equivalence-relation :
+    (S : equivalence-relation l2 A) →
+    relate-same-elements-equivalence-relation R S → (R ＝ S)
+  eq-relate-same-elements-equivalence-relation S =
+    map-inv-equiv (extensionality-equivalence-relation S)
+```

src/foundation.lagda.md

@@ -213,6 +213,7 @@ open import foundation.functoriality-sequential-limits public
 open import foundation.functoriality-set-quotients public
 open import foundation.functoriality-set-truncation public
 open import foundation.functoriality-truncation public
+open import foundation.fundamental-theorem-of-equivalence-relations public
 open import foundation.fundamental-theorem-of-identity-types public
 open import foundation.global-choice public
 open import foundation.global-subuniverses public