Cantor's theorem and diagonal argument

references.bib

@@ -92,13 +92,24 @@ @article{BW23
  keywords = {03B38 18N60 18N45 18D30 18N55 55U35 18N50 18D40 18D70,Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic}
 }
 
+@article{Cantor1890/91,
+ author = {Cantor, Georg},
+ journal = {Jahresbericht der Deutschen Mathematiker-Vereinigung},
+ pages = {72--78},
+ title = {Über eine elementare Frage der Mannigfaltigketislehre},
+ url = {http://eudml.org/doc/144383},
+ volume = {1},
+ year = {1890/91},
+ langid = {german}
+}
+
 @unpublished{Cisinski24,
- title = {Formalization of higher categories},
+ title  = {Formalization of higher categories},
  author = {Denis-Charles Cisinski, Bastiaan Cnossen, Kim Nguyen and Tashi Walde},
- date = {2024-08-10},
- year = {2024},
- month = {08},
- note = {\url{https://drive.google.com/file/d/1lKaq7watGGl3xvjqw9qHjm6SDPFJ2-0o/view}},
+ date  = {2024-08-10},
+ year  = {2024},
+ month  = {08},
+ note  = {\url{https://drive.google.com/file/d/1lKaq7watGGl3xvjqw9qHjm6SDPFJ2-0o/view}},
  annote = {}
 }
 
@@ -296,21 +307,21 @@ @inproceedings{KvR19
  eprintclass = {cs, math}
 }
 
-@incollection {Makkai98,
-  AUTHOR = {Makkai, M.},
- TITLE = {Towards a categorical foundation of mathematics},
- BOOKTITLE = {Logic {C}olloquium '95 ({H}aifa)},
-  SERIES = {Lecture Notes Logic},
-  VOLUME = {11},
- PAGES = {153--190},
- PUBLISHER = {Springer, Berlin},
- YEAR = {1998},
- ISBN = {3-540-63994-2},
-  MRCLASS = {03B15 (00A30 03A05 03G30 18A15 18D05)},
- MRNUMBER = {1678360},
-MRREVIEWER = {Peter\ Johnstone},
- DOI = {10.1007/978-3-662-22108-2\_11},
- URL = {https://doi.org/10.1007/978-3-662-22108-2_11},
+@incollection{Makkai98,
+ author  = {Makkai, M.},
+ title   = {Towards a categorical foundation of mathematics},
+  booktitle  = {Logic {C}olloquium '95 ({H}aifa)},
+ series  = {Lecture Notes Logic},
+ volume  = {11},
+ pages   = {153--190},
+  publisher  = {Springer, Berlin},
+ year   = {1998},
+ isbn   = {3-540-63994-2},
+ mrclass  = {03B15 (00A30 03A05 03G30 18A15 18D05)},
+ mrnumber  = {1678360},
+ mrreviewer = {Peter\ Johnstone},
+ doi   = {10.1007/978-3-662-22108-2\_11},
+ url  = {https://doi.org/10.1007/978-3-662-22108-2_11}
 }
 
 @book{May12,
@@ -558,23 +569,23 @@ @online{Shu14UniversalProperties
 }
 
 @article{Shu15,
- title = {Univalence for inverse diagrams and homotopy canonicity},
- author = {Shulman, Michael},
- date = {2015-06},
- year = {2015},
- month = {06},
- volume = {25},
- rights = {https://www.cambridge.org/core/terms},
- issn = {0960-1295, 1469-8072},
- doi = {10.1017/S0960129514000565},
- abstract = {We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (∞, 1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.},
- pages = {1203--1277},
- number = {5},
- journal = {Mathematical Structures in Computer Science},
- langid = {english},
- eprinttype  = {arxiv},
- eprintclass  = {math},
- eprint  = {1203.3253},
+ title  = {Univalence for inverse diagrams and homotopy canonicity},
+ author  = {Shulman, Michael},
+ date  = {2015-06},
+ year  = {2015},
+ month  = {06},
+ volume  = {25},
+ rights  = {https://www.cambridge.org/core/terms},
+ issn  = {0960-1295, 1469-8072},
+ doi  = {10.1017/S0960129514000565},
+ abstract  = {We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (∞, 1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.},
+ pages  = {1203--1277},
+ number  = {5},
+ journal  = {Mathematical Structures in Computer Science},
+ langid  = {english},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ eprint = {1203.3253}
 }
 
 @article{Shu17,

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

@@ -42,8 +42,9 @@ open import foundation.universe-levels
 ## Idea
 
 An integer `m` is said to **divide** an integer `n` if there exists an integer
-`k` equipped with an identification `km ＝ n`. Using the Curry-Howard
-interpretation of logic into type theory, we express divisibility as follows:
+`k` equipped with an identification `km ＝ n`. Using the
+[Curry–Howard interpretation](https://en.wikipedia.org/wiki/Curry–Howard_correspondence)
+of logic into type theory, we express divisibility as follows:
 
 ```text
  div-ℤ m n := Σ (k : ℤ), k *ℤ m ＝ n.

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

@@ -36,8 +36,8 @@ open import foundation.universe-levels
 
 A natural number `m` is said to **divide** a natural number `n` if there exists
 a natural number `k` equipped with an identification `km ＝ n`. Using the
-Curry-Howard interpretation of logic into type theory, we express divisibility
-as follows:
+[Curry–Howard interpretation](https://en.wikipedia.org/wiki/Curry–Howard_correspondence)
+of logic into type theory, we express divisibility as follows:
 
 ```text
  div-ℕ m n := Σ (k : ℕ), k *ℕ m ＝ n.

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

@@ -26,6 +26,7 @@ open import foundation.unit-type
 open import foundation.universe-levels
 
 open import foundation-core.decidable-propositions
+open import foundation-core.discrete-types
 open import foundation-core.torsorial-type-families
 ```
 
@@ -117,6 +118,9 @@ has-decidable-equality-ℕ : has-decidable-equality ℕ
 has-decidable-equality-ℕ x y =
  is-decidable-iff (eq-Eq-ℕ x y) Eq-eq-ℕ (is-decidable-Eq-ℕ x y)
 
+ℕ-Discrete-Type : Discrete-Type lzero
+ℕ-Discrete-Type = (ℕ , has-decidable-equality-ℕ)
+
 decidable-eq-ℕ : ℕ → ℕ → Decidable-Prop lzero
 pr1 (decidable-eq-ℕ m n) = (m ＝ n)
 pr1 (pr2 (decidable-eq-ℕ m n)) = is-set-ℕ m n

src/foundation-core/decidable-propositions.lagda.md

@@ -154,6 +154,31 @@ module _
  pr2 product-Decidable-Prop = is-decidable-prop-product-Decidable-Prop
 ```
 
+### The negation operation on decidable propositions
+
+```agda
+is-decidable-prop-neg :
+ {l1 : Level} {A : UU l1} → is-decidable A → is-decidable-prop (¬ A)
+is-decidable-prop-neg is-decidable-A =
+ ( is-prop-neg , is-decidable-neg is-decidable-A)
+
+neg-type-Decidable-Prop :
+ {l1 : Level} (A : UU l1) → is-decidable A → Decidable-Prop l1
+neg-type-Decidable-Prop A is-decidable-A =
+ ( ¬ A , is-decidable-prop-neg is-decidable-A)
+
+neg-Decidable-Prop :
+ {l1 : Level} → Decidable-Prop l1 → Decidable-Prop l1
+neg-Decidable-Prop P =
+ neg-type-Decidable-Prop
+ ( type-Decidable-Prop P)
+ ( is-decidable-Decidable-Prop P)
+
+type-neg-Decidable-Prop :
+ {l1 : Level} → Decidable-Prop l1 → UU l1
+type-neg-Decidable-Prop P = type-Decidable-Prop (neg-Decidable-Prop P)
+```
+
 ### Decidability of a propositional truncation
 
 ```agda

src/foundation-core/discrete-types.lagda.md

@@ -18,7 +18,9 @@ open import foundation-core.sets
 
 ## Idea
 
-A discrete type is a type that has decidable equality.
+A {{#concept "discrete type" Agda=Discrete-Type}} is a type that has
+[decidable equality](foundation.decidable-equality.md). Consequently, discrete
+types are [sets](foundation-core.sets.md) by Hedberg's theorem.
 
 ## Definition
 
@@ -45,3 +47,8 @@ module _
  pr1 set-Discrete-Type = type-Discrete-Type
  pr2 set-Discrete-Type = is-set-type-Discrete-Type
 ```
+
+## External links
+
+- [classical set](https://ncatlab.org/nlab/show/classical+set) at $n$Lab
+- [decidable object](https://ncatlab.org/nlab/show/decidable+object) at $n$Lab

src/foundation-core/negation.lagda.md

@@ -16,8 +16,10 @@ open import foundation-core.empty-types
 
 ## Idea
 
-The Curry-Howard interpretation of _negation_ in type theory is the
-interpretation of the proposition `P ⇒ ⊥` using propositions as types. Thus, the
+The
+[Curry–Howard interpretation](https://en.wikipedia.org/wiki/Curry–Howard_correspondence)
+of _negation_ in type theory is the interpretation of the proposition `P ⇒ ⊥`
+using propositions as types. Thus, the
 {{#concept "negation" Disambiguation="of a type" WDID=Q190558 WD="logical negation" Agda=¬_}}
 of a type `A` is the type `A → empty`.
 

src/foundation-core/subtypes.lagda.md

@@ -315,7 +315,7 @@ equiv-type-subtype :
  ( Σ A P) ≃ (Σ A Q)
 pr1 (equiv-type-subtype is-subtype-P is-subtype-Q f g) = tot f
 pr2 (equiv-type-subtype is-subtype-P is-subtype-Q f g) =
- is-equiv-tot-is-fiberwise-equiv {f = f}
+ is-equiv-tot-is-fiberwise-equiv
  ( λ x →
  is-equiv-has-converse-is-prop
  ( is-subtype-P x)
@@ -359,7 +359,7 @@ abstract
  (is-subtype-P : is-subtype P) (is-subtype-Q : is-subtype Q)
  (f : A → B) (g : (x : A) → P x → Q (f x)) →
  (is-equiv-f : is-equiv f) →
- ((y : B) → (Q y) → P (map-inv-is-equiv is-equiv-f y)) →
+ ((y : B) → Q y → P (map-inv-is-equiv is-equiv-f y)) →
  is-equiv (map-Σ Q f g)
  is-equiv-subtype-is-equiv' {P = P} {Q}
  is-subtype-P is-subtype-Q f g is-equiv-f h =

src/foundation-core/type-theoretic-principle-of-choice.lagda.md

@@ -24,9 +24,11 @@ A dependent function taking values in a
 [dependent pair type](foundation.dependent-pair-types.md) is
 [equivalently](foundation-core.equivalences.md) described as a pair of dependent
 functions. This equivalence, which gives the distributivity of Π over Σ, is also
-known as the **type theoretic principle of choice**. Indeed, it is the
-Curry-Howard interpretation of (one formulation of) the
-[axiom of choice](foundation.axiom-of-choice.md).
+known as the
+{{#concept "type theoretic principle of choice" Agda=distributive-Π-Σ}}. Indeed,
+it is the
+[Curry–Howard interpretation](https://en.wikipedia.org/wiki/Curry–Howard_correspondence)
+of (one formulation of) the [axiom of choice](foundation.axiom-of-choice.md).
 
 We establish this equivalence both for explicit and implicit function types.
 
@@ -188,3 +190,8 @@ module _
  pr1 equiv-mapping-into-Σ = mapping-into-Σ
  pr2 equiv-mapping-into-Σ = is-equiv-mapping-into-Σ
 ```
+
+## External links
+
+- [type theoretic axiom of choice](https://ncatlab.org/nlab/show/type+theoretic+axiom+of+choice)
+ at $n$Lab

src/foundation.lagda.md

@@ -44,7 +44,7 @@ open import foundation.binary-transport public
 open import foundation.binary-type-duality public
 open import foundation.booleans public
 open import foundation.cantor-schroder-bernstein-escardo public
-open import foundation.cantors-diagonal-argument public
+open import foundation.cantors-theorem public
 open import foundation.cartesian-morphisms-arrows public
 open import foundation.cartesian-morphisms-span-diagrams public
 open import foundation.cartesian-product-types public

src/foundation/booleans.lagda.md

@@ -234,6 +234,9 @@ pr2 bool-𝔽 = is-finite-bool
 neq-neg-bool : (b : bool) → b ≠ neg-bool b
 neq-neg-bool true ()
 neq-neg-bool false ()
+
+neq-neg-bool' : (b : bool) → neg-bool b ≠ b
+neq-neg-bool' b = neq-neg-bool b ∘ inv
 ```
 
 ### Boolean negation is an involution