100 Theorems (#1201)

Adds a page about our progress on [_Formalizing 100
Theorems_](https://www.cs.ru.nl/~freek/100/).

HOWTO-INSTALL.md

@@ -303,7 +303,7 @@ below to ensure a smooth setup and workflow. Also, please make sure to follow
 our [coding style](CODINGSTYLE.md) and
 [design principles](DESIGN-PRINCIPLES.md).
 
-### <a name="pre-commit-hooks"></a>Pre-commit hooks and Python dependencies
+### Pre-commit hooks and Python dependencies {#pre-commit-hooks}
 
 The agda-unimath library includes [pre-commit](https://pre-commit.com/) hooks
 that enforce [basic formatting rules](CONTRIBUTING.md). These will inform you of
@@ -333,7 +333,7 @@ Keep in mind that `pre-commit` is also a part of the Continuous Integration
 (CI), so any PR that violates the enforced conventions will be automatically
 blocked from merging.
 
-### <a name="build-website"></a>Building and viewing the website locally
+### Building and viewing the website locally {#build-website}
 
 The build process for the website uses the
 [Rust language](https://www.rust-lang.org/)'s package manager `cargo`. To

references.bib

@@ -1,3 +1,15 @@
+@online{1000+theorems,
+  title  = {1000+ theorems},
+  author = {Freek Wiedijk},
+  url    = {https://1000-plus.github.io/}
+}
+
+@online{100theorems,
+  title  = {Formalizing 100 Theorems},
+  author = {Freek Wiedijk},
+  url    = {https://www.cs.ru.nl/~freek/100/}
+}
+
 @article{AKS15,
   title       = {Univalent Categories and the {{Rezk}} Completion},
   author      = {Ahrens, Benedikt and Kapulkin, Krzysztof and Shulman, Michael},

src/elementary-number-theory/integer-fractions.lagda.md

@@ -24,15 +24,17 @@ open import foundation.negation
 open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
+
+open import set-theory.countable-sets
 ```
 
 </details>
 
 ## Idea
 
-The type of integer fractions is the type of pairs `n/m` consisting of an
-integer `n` and a positive integer `m`. The type of rational numbers is a
-retract of the type of fractions.
+The type of {{#concept "integer fractions" Agda=fraction-ℤ}} is the type of
+pairs `n/m` consisting of an integer `n` and a positive integer `m`. The type of
+rational numbers is a retract of the type of fractions.
 
 ## Definitions
 
@@ -122,6 +124,9 @@ abstract
 abstract
   is-set-fraction-ℤ : is-set fraction-ℤ
   is-set-fraction-ℤ = is-set-Σ is-set-ℤ (λ _ → is-set-positive-ℤ)
+
+fraction-ℤ-Set : Set lzero
+fraction-ℤ-Set = fraction-ℤ , is-set-fraction-ℤ
 ```
 
 ```agda
@@ -260,3 +265,15 @@ abstract
     is-nonzero-is-positive-ℤ
       ( is-positive-gcd-numerator-denominator-fraction-ℤ x)
 ```
+
+### The set of integer fractions is countable
+
+```agda
+is-countable-fraction-ℤ : is-countable fraction-ℤ-Set
+is-countable-fraction-ℤ =
+  is-countable-product
+    ( ℤ-Set)
+    ( positive-ℤ-Set)
+    ( is-countable-ℤ)
+    ( is-countable-positive-ℤ)
+```

src/elementary-number-theory/positive-integers.lagda.md

@@ -18,16 +18,20 @@ open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.equivalences
+open import foundation.existential-quantification
 open import foundation.function-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.retractions
 open import foundation.sections
 open import foundation.sets
 open import foundation.subtypes
+open import foundation.surjective-maps
 open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
+
+open import set-theory.countable-sets
 ```
 
 </details>
@@ -122,6 +126,9 @@ is-nonzero-is-positive-ℤ {inr (inr x)} H ()
 is-set-positive-ℤ : is-set positive-ℤ
 is-set-positive-ℤ =
   is-set-type-subtype subtype-positive-ℤ is-set-ℤ
+
+positive-ℤ-Set : Set lzero
+positive-ℤ-Set = positive-ℤ , is-set-positive-ℤ
 ```
 
 ### The successor of a positive integer is positive
@@ -182,6 +189,19 @@ pr1 equiv-positive-int-ℕ = positive-int-ℕ
 pr2 equiv-positive-int-ℕ = is-equiv-positive-int-ℕ
 ```
 
+### The set of positive integers is countable
+
+```agda
+is-countable-positive-ℤ : is-countable positive-ℤ-Set
+is-countable-positive-ℤ =
+  is-countable-is-directly-countable
+    ( positive-ℤ-Set)
+    ( one-positive-ℤ)
+    ( intro-exists
+      ( positive-int-ℕ)
+      ( is-surjective-is-equiv is-equiv-positive-int-ℕ))
+```
+
 ## See also
 
 - The relations between positive and nonnegative, negative and nonnpositive

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

@@ -25,9 +25,14 @@ open import foundation.identity-types
 open import foundation.negation
 open import foundation.propositions
 open import foundation.reflecting-maps-equivalence-relations
+open import foundation.retracts-of-types
+open import foundation.sections
 open import foundation.sets
 open import foundation.subtypes
+open import foundation.surjective-maps
 open import foundation.universe-levels
+
+open import set-theory.countable-sets
 ```
 
 </details>
@@ -157,18 +162,41 @@ abstract
 ℚ-Set : Set lzero
 pr1 ℚ-Set = ℚ
 pr2 ℚ-Set = is-set-ℚ
+```
+
+### The rationals are a retract of the integer fractions
 
+```agda
 abstract
   is-retraction-rational-fraction-ℚ :
     (x : ℚ) → rational-fraction-ℤ (fraction-ℚ x) ＝ x
-  is-retraction-rational-fraction-ℚ (pair (pair m (pair n n-pos)) p) =
+  is-retraction-rational-fraction-ℚ ((m , n , n-pos) , p) =
     eq-pair-Σ
       ( eq-pair
         ( eq-quotient-div-is-one-ℤ _ _ p (div-left-gcd-ℤ m n))
         ( eq-pair-Σ
           ( eq-quotient-div-is-one-ℤ _ _ p (div-right-gcd-ℤ m n))
           ( eq-is-prop (is-prop-is-positive-ℤ n))))
       ( eq-is-prop (is-prop-is-reduced-fraction-ℤ (m , n , n-pos)))
+
+section-rational-fraction-ℤ : section rational-fraction-ℤ
+section-rational-fraction-ℤ = (fraction-ℚ , is-retraction-rational-fraction-ℚ)
+
+retract-integer-fraction-ℚ : ℚ retract-of fraction-ℤ
+retract-integer-fraction-ℚ =
+  ( fraction-ℚ , rational-fraction-ℤ , is-retraction-rational-fraction-ℚ)
+```
+
+### The rationals are countable
+
+```agda
+is-countable-ℚ : is-countable ℚ-Set
+is-countable-ℚ =
+  is-countable-retract-of
+    ( fraction-ℤ-Set)
+    ( ℚ-Set)
+    ( retract-integer-fraction-ℚ)
+    ( is-countable-fraction-ℤ)
 ```
 
 ### Two fractions with the same numerator and same denominator are equal

src/foundation/cantor-schroder-bernstein-escardo.lagda.md

@@ -10,6 +10,7 @@ module foundation.cantor-schroder-bernstein-escardo where
 open import foundation.action-on-identifications-functions
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
+open import foundation.injective-maps
 open import foundation.law-of-excluded-middle
 open import foundation.perfect-images
 open import foundation.split-surjective-maps
@@ -21,8 +22,8 @@ open import foundation-core.empty-types
 open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.identity-types
-open import foundation-core.injective-maps
 open import foundation-core.negation
+open import foundation-core.sets
 ```
 
 </details>
@@ -172,6 +173,21 @@ module _
     is-equiv-map-Cantor-Schröder-Bernstein-Escardó f g
 ```
 
+## Corollaries
+
+### The Cantor–Schröder–Bernstein theorem
+
+```agda
+Cantor-Schröder-Bernstein :
+  {l1 l2 : Level} (lem : LEM (l1 ⊔ l2))
+  (A : Set l1) (B : Set l2) →
+  injection (type-Set A) (type-Set B) →
+  injection (type-Set B) (type-Set A) →
+  (type-Set A) ≃ (type-Set B)
+Cantor-Schröder-Bernstein lem A B f g =
+  Cantor-Schröder-Bernstein-Escardó lem (emb-injection B f) (emb-injection A g)
+```
+
 ## References
 
 - Escardó's formalizations regarding this theorem can be found at

src/foundation/injective-maps.lagda.md

@@ -15,6 +15,7 @@ open import foundation.universe-levels
 
 open import foundation-core.embeddings
 open import foundation-core.empty-types
+open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.identity-types
 open import foundation-core.negation
 open import foundation-core.propositional-maps
@@ -83,6 +84,11 @@ module _
       {f : A → B} → is-set B → is-injective f → is-prop-map f
     is-prop-map-is-injective {f} H I =
       is-prop-map-is-emb (is-emb-is-injective H I)
+
+emb-injection :
+  {l1 l2 : Level} {A : UU l1} (B : Set l2) →
+  injection A (type-Set B) → A ↪ (type-Set B)
+emb-injection B = tot (λ f → is-emb-is-injective (is-set-type-Set B))
 ```
 
 ### For a map between sets, being injective is a property

src/foundation/maybe.lagda.md

@@ -7,11 +7,13 @@ module foundation.maybe where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
 open import foundation.coproduct-types
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.equality-coproduct-types
+open import foundation.existential-quantification
 open import foundation.propositional-truncations
 open import foundation.surjective-maps
 open import foundation.type-arithmetic-empty-type
@@ -49,6 +51,22 @@ not [idempotent](foundation.idempotent-maps.md).
 ```agda
 Maybe : {l : Level} → UU l → UU l
 Maybe X = X + unit
+
+unit-Maybe : {l : Level} {X : UU l} → X → Maybe X
+unit-Maybe = inl
+
+exception-Maybe : {l : Level} {X : UU l} → Maybe X
+exception-Maybe = inr star
+
+extend-Maybe :
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} → (X → Maybe Y) → Maybe X → Maybe Y
+extend-Maybe f (inl x) = f x
+extend-Maybe f (inr *) = inr *
+
+map-Maybe :
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} → (X → Y) → Maybe X → Maybe Y
+map-Maybe f (inl x) = inl (f x)
+map-Maybe f (inr *) = inr *
 ```
 
 ### The inductive definition of the maybe monad
@@ -59,12 +77,6 @@ data Maybe' {l : Level} (X : UU l) : UU l where
   exception-Maybe' : Maybe' X
 
 {-# BUILTIN MAYBE Maybe' #-}
-
-unit-Maybe : {l : Level} {X : UU l} → X → Maybe X
-unit-Maybe = inl
-
-exception-Maybe : {l : Level} {X : UU l} → Maybe X
-exception-Maybe {l} {X} = inr star
 ```
 
 ### The predicate of being an exception
@@ -148,7 +160,7 @@ abstract
 ```agda
 decide-Maybe :
   {l : Level} {X : UU l} (x : Maybe X) → is-value-Maybe x + is-exception-Maybe x
-decide-Maybe (inl x) = inl (pair x refl)
+decide-Maybe (inl x) = inl (x , refl)
 decide-Maybe (inr star) = inr refl
 ```
 
@@ -159,7 +171,7 @@ abstract
   is-not-exception-is-value-Maybe :
     {l1 : Level} {X : UU l1} (x : Maybe X) →
     is-value-Maybe x → is-not-exception-Maybe x
-  is-not-exception-is-value-Maybe {l1} {X} .(inl x) (pair x refl) =
+  is-not-exception-is-value-Maybe {l1} {X} .(inl x) (x , refl) =
     is-not-exception-unit-Maybe x
 ```
 
@@ -224,6 +236,39 @@ module _
   equiv-Maybe-Maybe' = (map-Maybe-Maybe' , is-equiv-map-Maybe-Maybe')
 ```
 
+### The extension of surjective maps is surjective
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  is-surjective-extend-is-surjective-Maybe :
+    {f : A → Maybe B} → is-surjective f → is-surjective (extend-Maybe f)
+  is-surjective-extend-is-surjective-Maybe {f} F y =
+    elim-exists
+      ( exists-structure-Prop (Maybe A) (λ z → extend-Maybe f z ＝ y))
+      ( λ x p → intro-exists (inl x) p)
+      ( F y)
+```
+
+### The functorial action of `Maybe` preserves surjective maps
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  is-surjective-map-is-surjective-Maybe :
+    {f : A → B} → is-surjective f → is-surjective (map-Maybe f)
+  is-surjective-map-is-surjective-Maybe {f} F (inl y) =
+    elim-exists
+      ( exists-structure-Prop (Maybe A) (λ z → map-Maybe f z ＝ inl y))
+      ( λ x p → intro-exists (inl x) (ap inl p))
+      ( F y)
+  is-surjective-map-is-surjective-Maybe F (inr *) = intro-exists (inr *) refl
+```
+
 ### There is a surjection from `Maybe A + Maybe B` to `Maybe (A + B)`
 
 ```agda

src/literature.lagda.md

@@ -1,18 +1,20 @@
 # Formalization of results from the literature
 
-> This page is a work in early progress. To see what's happening behind the
-> scenes, you can have a look at the associated GitHub issue
+> This page is currently under construction. To see what's happening behind the
+> scenes, see the associated GitHub issue
 > [#1055](https://github.com/UniMath/agda-unimath/issues/1055).
 
-## References
-
-{{#bibliography}} {{#reference SvDR20}} {{#reference Shu17}}
-
-## Files in the namespace
+## Modules in the literature namespace
 
 ```agda
 module literature where
 
+open import literature.100-theorems public
 open import literature.idempotents-in-intensional-type-theory public
 open import literature.sequential-colimits-in-homotopy-type-theory public
 ```
+
+## References
+
+{{#bibliography}} {{#reference SvDR20}} {{#reference Shu17}}
+{{#reference 100theorems}}