Peano arithmetic (#876)

Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>

src/elementary-number-theory.lagda.md

@@ -92,6 +92,7 @@ open import elementary-number-theory.nonzero-integers public
 open import elementary-number-theory.nonzero-natural-numbers public
 open import elementary-number-theory.ordinal-induction-natural-numbers public
 open import elementary-number-theory.parity-natural-numbers public
+open import elementary-number-theory.peano-arithmetic public
 open import elementary-number-theory.pisano-periods public
 open import elementary-number-theory.poset-of-natural-numbers-ordered-by-divisibility public
 open import elementary-number-theory.powers-integers public

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

@@ -7,6 +7,7 @@ module elementary-number-theory.addition-natural-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-binary-functions

src/elementary-number-theory/based-strong-induction-natural-numbers.lagda.md

@@ -8,6 +8,7 @@ module elementary-number-theory.based-strong-induction-natural-numbers where
 
 ```agda
 open import elementary-number-theory.based-induction-natural-numbers
+open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.natural-numbers
 

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

@@ -10,16 +10,19 @@ module elementary-number-theory.equality-natural-numbers where
 open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions
-open import foundation.contractible-types
 open import foundation.coproduct-types
 open import foundation.decidable-equality
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
+open import foundation.empty-types
 open import foundation.equivalences
 open import foundation.function-types
 open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.propositions
 open import foundation.set-truncations
+open import foundation.sets
 open import foundation.unit-type
 open import foundation.universe-levels
 
@@ -29,8 +32,78 @@ open import foundation-core.torsorial-type-families
 
 </details>
 
+## Definitions
+
+### Observational equality on the natural numbers
+
+```agda
+Eq-ℕ : ℕ → ℕ → UU lzero
+Eq-ℕ zero-ℕ zero-ℕ = unit
+Eq-ℕ zero-ℕ (succ-ℕ n) = empty
+Eq-ℕ (succ-ℕ m) zero-ℕ = empty
+Eq-ℕ (succ-ℕ m) (succ-ℕ n) = Eq-ℕ m n
+```
+
 ## Properties
 
+### The type of natural numbers is a set
+
+```agda
+abstract
+  is-prop-Eq-ℕ :
+    (n m : ℕ) → is-prop (Eq-ℕ n m)
+  is-prop-Eq-ℕ zero-ℕ zero-ℕ = is-prop-unit
+  is-prop-Eq-ℕ zero-ℕ (succ-ℕ m) = is-prop-empty
+  is-prop-Eq-ℕ (succ-ℕ n) zero-ℕ = is-prop-empty
+  is-prop-Eq-ℕ (succ-ℕ n) (succ-ℕ m) = is-prop-Eq-ℕ n m
+
+refl-Eq-ℕ : (n : ℕ) → Eq-ℕ n n
+refl-Eq-ℕ zero-ℕ = star
+refl-Eq-ℕ (succ-ℕ n) = refl-Eq-ℕ n
+
+Eq-eq-ℕ : {x y : ℕ} → x ＝ y → Eq-ℕ x y
+Eq-eq-ℕ {x} {.x} refl = refl-Eq-ℕ x
+
+eq-Eq-ℕ : (x y : ℕ) → Eq-ℕ x y → x ＝ y
+eq-Eq-ℕ zero-ℕ zero-ℕ e = refl
+eq-Eq-ℕ (succ-ℕ x) (succ-ℕ y) e = ap succ-ℕ (eq-Eq-ℕ x y e)
+
+abstract
+  is-set-ℕ : is-set ℕ
+  is-set-ℕ =
+    is-set-prop-in-id
+      Eq-ℕ
+      is-prop-Eq-ℕ
+      refl-Eq-ℕ
+      eq-Eq-ℕ
+
+ℕ-Set : Set lzero
+pr1 ℕ-Set = ℕ
+pr2 ℕ-Set = is-set-ℕ
+```
+
+### The property of being zero
+
+```agda
+is-prop-is-zero-ℕ : (n : ℕ) → is-prop (is-zero-ℕ n)
+is-prop-is-zero-ℕ n = is-set-ℕ n zero-ℕ
+
+is-zero-ℕ-Prop : ℕ → Prop lzero
+pr1 (is-zero-ℕ-Prop n) = is-zero-ℕ n
+pr2 (is-zero-ℕ-Prop n) = is-prop-is-zero-ℕ n
+```
+
+### The property of being one
+
+```agda
+is-prop-is-one-ℕ : (n : ℕ) → is-prop (is-one-ℕ n)
+is-prop-is-one-ℕ n = is-set-ℕ n 1
+
+is-one-ℕ-Prop : ℕ → Prop lzero
+pr1 (is-one-ℕ-Prop n) = is-one-ℕ n
+pr2 (is-one-ℕ-Prop n) = is-prop-is-one-ℕ n
+```
+
 ### The type of natural numbers has decidable equality
 
 ```agda
@@ -72,13 +145,13 @@ is-decidable-is-not-one-ℕ x =
   is-decidable-neg (is-decidable-is-one-ℕ x)
 ```
 
-## The full characterization of the identity type of ℕ
+## The full characterization of the identity type of `ℕ`
 
 ```agda
 map-total-Eq-ℕ :
   (m : ℕ) → Σ ℕ (Eq-ℕ m) → Σ ℕ (Eq-ℕ (succ-ℕ m))
-pr1 (map-total-Eq-ℕ m (pair n e)) = succ-ℕ n
-pr2 (map-total-Eq-ℕ m (pair n e)) = e
+pr1 (map-total-Eq-ℕ m (n , e)) = succ-ℕ n
+pr2 (map-total-Eq-ℕ m (n , e)) = e
 
 is-torsorial-Eq-ℕ :
   (m : ℕ) → is-torsorial (Eq-ℕ m)

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

@@ -8,6 +8,7 @@ module elementary-number-theory.factorials where
 
 ```agda
 open import elementary-number-theory.divisibility-natural-numbers
+open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers

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

@@ -7,6 +7,7 @@ module elementary-number-theory.integers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions

src/elementary-number-theory/monoid-of-natural-numbers-with-addition.lagda.md

@@ -8,7 +8,7 @@ module elementary-number-theory.monoid-of-natural-numbers-with-addition where
 
 ```agda
 open import elementary-number-theory.addition-natural-numbers
-open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.equality-natural-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.universe-levels

src/elementary-number-theory/monoid-of-natural-numbers-with-maximum.lagda.md

@@ -7,6 +7,7 @@ module elementary-number-theory.monoid-of-natural-numbers-with-maximum where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.initial-segments-natural-numbers
 open import elementary-number-theory.maximum-natural-numbers
 open import elementary-number-theory.natural-numbers

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

@@ -8,6 +8,7 @@ module elementary-number-theory.multiplication-natural-numbers where
 
 ```agda
 open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-binary-functions

src/elementary-number-theory/multiplicative-monoid-of-natural-numbers.lagda.md

@@ -7,8 +7,8 @@ module elementary-number-theory.multiplicative-monoid-of-natural-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
-open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.universe-levels

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

@@ -7,31 +7,21 @@ module elementary-number-theory.natural-numbers where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
-open import foundation.equivalences
-open import foundation.function-types
-open import foundation.homotopies
-open import foundation.identity-types
-open import foundation.injective-maps
-open import foundation.logical-equivalences
-open import foundation.negated-equality
-open import foundation.negation
-open import foundation.unit-type
 open import foundation.universe-levels
 
-open import foundation-core.coproduct-types
 open import foundation-core.empty-types
-open import foundation-core.propositions
-open import foundation-core.sets
+open import foundation-core.identity-types
+open import foundation-core.injective-maps
+open import foundation-core.negation
 ```
 
 </details>
 
 ## Idea
 
-The type of natural numbers is inductively generated by the zero element and the
-successor function. The induction principle for the natural numbers works to
+The **natural numbers** is an inductively generated type by the zero element and
+the successor function. The induction principle for the natural numbers works to
 construct sections of type families over the natural numbers.
 
 ## Definitions
@@ -86,30 +76,27 @@ is-not-one-ℕ' n = ¬ (is-one-ℕ' n)
 ind-ℕ :
   {l : Level} {P : ℕ → UU l} →
   P 0 → ((n : ℕ) → P n → P (succ-ℕ n)) → ((n : ℕ) → P n)
-ind-ℕ p0 pS 0 = p0
-ind-ℕ p0 pS (succ-ℕ n) = pS n (ind-ℕ p0 pS n)
+ind-ℕ p-zero p-succ 0 = p-zero
+ind-ℕ p-zero p-succ (succ-ℕ n) = p-succ n (ind-ℕ p-zero p-succ n)
 ```
 
-### Peano's 7th axiom
+### The recursion principle of ℕ
+
+```agda
+rec-ℕ : {l : Level} {A : UU l} → A → (ℕ → A → A) → (ℕ → A)
+rec-ℕ = ind-ℕ
+```
+
+### The successor function on ℕ is injective
 
 ```agda
 is-injective-succ-ℕ : is-injective succ-ℕ
 is-injective-succ-ℕ refl = refl
-
-private
-  Peano-7 :
-    (x y : ℕ) → (x ＝ y) ↔ (succ-ℕ x ＝ succ-ℕ y)
-  pr1 (Peano-7 x y) refl = refl
-  pr2 (Peano-7 x y) = is-injective-succ-ℕ
 ```
 
-### Peano's 8th axiom
+### Successors are nonzero
 
 ```agda
-private
-  Peano-8 : (x : ℕ) → is-nonzero-ℕ (succ-ℕ x)
-  Peano-8 x ()
-
 is-nonzero-succ-ℕ : (x : ℕ) → is-nonzero-ℕ (succ-ℕ x)
 is-nonzero-succ-ℕ x ()
 
@@ -121,11 +108,11 @@ is-successor-is-nonzero-ℕ {zero-ℕ} H = ex-falso (H refl)
 pr1 (is-successor-is-nonzero-ℕ {succ-ℕ x} H) = x
 pr2 (is-successor-is-nonzero-ℕ {succ-ℕ x} H) = refl
 
-has-no-fixed-points-succ-ℕ : (x : ℕ) → succ-ℕ x ≠ x
+has-no-fixed-points-succ-ℕ : (x : ℕ) → ¬ (succ-ℕ x ＝ x)
 has-no-fixed-points-succ-ℕ x ()
 ```
 
-### Basic inequalities
+### Basic nonequalities
 
 ```agda
 is-nonzero-one-ℕ : is-nonzero-ℕ 1
@@ -135,98 +122,12 @@ is-not-one-zero-ℕ : is-not-one-ℕ zero-ℕ
 is-not-one-zero-ℕ ()
 
 is-nonzero-two-ℕ : is-nonzero-ℕ 2
-is-nonzero-two-ℕ = is-nonzero-succ-ℕ 1
+is-nonzero-two-ℕ ()
 
 is-not-one-two-ℕ : is-not-one-ℕ 2
 is-not-one-two-ℕ ()
 ```
 
-### The type of natural numbers is a set
-
-```agda
-Eq-ℕ : ℕ → ℕ → UU lzero
-Eq-ℕ zero-ℕ zero-ℕ = unit
-Eq-ℕ zero-ℕ (succ-ℕ n) = empty
-Eq-ℕ (succ-ℕ m) zero-ℕ = empty
-Eq-ℕ (succ-ℕ m) (succ-ℕ n) = Eq-ℕ m n
-
-abstract
-  is-prop-Eq-ℕ :
-    (n m : ℕ) → is-prop (Eq-ℕ n m)
-  is-prop-Eq-ℕ zero-ℕ zero-ℕ = is-prop-unit
-  is-prop-Eq-ℕ zero-ℕ (succ-ℕ m) = is-prop-empty
-  is-prop-Eq-ℕ (succ-ℕ n) zero-ℕ = is-prop-empty
-  is-prop-Eq-ℕ (succ-ℕ n) (succ-ℕ m) = is-prop-Eq-ℕ n m
-
-refl-Eq-ℕ : (n : ℕ) → Eq-ℕ n n
-refl-Eq-ℕ zero-ℕ = star
-refl-Eq-ℕ (succ-ℕ n) = refl-Eq-ℕ n
-
-Eq-eq-ℕ : {x y : ℕ} → x ＝ y → Eq-ℕ x y
-Eq-eq-ℕ {x} {.x} refl = refl-Eq-ℕ x
-
-eq-Eq-ℕ : (x y : ℕ) → Eq-ℕ x y → x ＝ y
-eq-Eq-ℕ zero-ℕ zero-ℕ e = refl
-eq-Eq-ℕ (succ-ℕ x) (succ-ℕ y) e = ap succ-ℕ (eq-Eq-ℕ x y e)
-
-abstract
-  is-set-ℕ : is-set ℕ
-  is-set-ℕ =
-    is-set-prop-in-id
-      Eq-ℕ
-      is-prop-Eq-ℕ
-      refl-Eq-ℕ
-      eq-Eq-ℕ
-
-ℕ-Set : Set lzero
-pr1 ℕ-Set = ℕ
-pr2 ℕ-Set = is-set-ℕ
-
-is-prop-is-zero-ℕ : (n : ℕ) → is-prop (is-zero-ℕ n)
-is-prop-is-zero-ℕ n = is-set-ℕ n zero-ℕ
-
-is-zero-ℕ-Prop : ℕ → Prop lzero
-pr1 (is-zero-ℕ-Prop n) = is-zero-ℕ n
-pr2 (is-zero-ℕ-Prop n) = is-prop-is-zero-ℕ n
-
-is-prop-is-one-ℕ : (n : ℕ) → is-prop (is-one-ℕ n)
-is-prop-is-one-ℕ n = is-set-ℕ n 1
-
-is-one-ℕ-Prop : ℕ → Prop lzero
-pr1 (is-one-ℕ-Prop n) = is-one-ℕ n
-pr2 (is-one-ℕ-Prop n) = is-prop-is-one-ℕ n
-```
-
-### The natural numbers is a fixpoint to the functor `X ↦ 1 + X`
-
-```agda
-map-equiv-ℕ : ℕ → unit + ℕ
-map-equiv-ℕ zero-ℕ = inl star
-map-equiv-ℕ (succ-ℕ n) = inr n
-
-map-inv-equiv-ℕ : unit + ℕ → ℕ
-map-inv-equiv-ℕ (inl x) = zero-ℕ
-map-inv-equiv-ℕ (inr n) = succ-ℕ n
-
-is-retraction-map-inv-equiv-ℕ :
-  ( map-inv-equiv-ℕ ∘ map-equiv-ℕ) ~ id
-is-retraction-map-inv-equiv-ℕ zero-ℕ = refl
-is-retraction-map-inv-equiv-ℕ (succ-ℕ n) = refl
-
-is-section-map-inv-equiv-ℕ :
-  ( map-equiv-ℕ ∘ map-inv-equiv-ℕ) ~ id
-is-section-map-inv-equiv-ℕ (inl star) = refl
-is-section-map-inv-equiv-ℕ (inr n) = refl
-
-equiv-ℕ : ℕ ≃ (unit + ℕ)
-pr1 equiv-ℕ = map-equiv-ℕ
-pr2 equiv-ℕ =
-  is-equiv-is-invertible
-    map-inv-equiv-ℕ
-    is-section-map-inv-equiv-ℕ
-    is-retraction-map-inv-equiv-ℕ
-```
-
 ## See also
 
 - The based induction principle is defined in

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

@@ -8,6 +8,7 @@ module elementary-number-theory.parity-natural-numbers where
 
 ```agda
 open import elementary-number-theory.divisibility-natural-numbers
+open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.modular-arithmetic-standard-finite-types
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers