-
Notifications
You must be signed in to change notification settings - Fork 72
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Coinductive definition of the conatural numbers (#1232)
- Loading branch information
1 parent
6152336
commit 4545c3a
Showing
13 changed files
with
822 additions
and
31 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
172 changes: 172 additions & 0 deletions
172
src/elementary-number-theory/conatural-numbers.lagda.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,172 @@ | ||
| # Conatural numbers | ||
|
|
||
| ```agda | ||
| {-# OPTIONS --guardedness #-} | ||
|
|
||
| module elementary-number-theory.conatural-numbers where | ||
| ``` | ||
|
|
||
| <details><summary>Imports</summary> | ||
|
|
||
| ```agda | ||
| open import foundation.action-on-identifications-functions | ||
| open import foundation.coproduct-types | ||
| open import foundation.dependent-pair-types | ||
| open import foundation.homotopies | ||
| open import foundation.injective-maps | ||
| open import foundation.maybe | ||
| open import foundation.negated-equality | ||
| open import foundation.retractions | ||
| open import foundation.sections | ||
| open import foundation.universe-levels | ||
|
|
||
| open import foundation-core.identity-types | ||
| ``` | ||
|
|
||
| </details> | ||
|
|
||
| ## Idea | ||
|
|
||
| The {{#concept "conatural numbers" Agda=ℕ∞}} `ℕ∞` is a | ||
| [set](foundation-core.sets.md) that satisfies the dual of the universal property | ||
| of [natural numbers](elementary-number-theory.natural-numbers.md) in the sense | ||
| that it is the final coalgebra of the functor `X ↦ 1 + X` rather than the | ||
| initial algebra. | ||
|
|
||
| ## Definitions | ||
|
|
||
| ### The coinductive type of conatural numbers | ||
|
|
||
| ```agda | ||
| record ℕ∞ : UU lzero | ||
| where | ||
| coinductive | ||
| field | ||
| decons-ℕ∞ : Maybe ℕ∞ | ||
|
|
||
| open ℕ∞ public | ||
| ``` | ||
|
|
||
| ### The zero element of the conatural numbers | ||
|
|
||
| ```agda | ||
| zero-ℕ∞ : ℕ∞ | ||
| decons-ℕ∞ zero-ℕ∞ = exception-Maybe | ||
| ``` | ||
|
|
||
| ### The element at infinity of the conatural numbers | ||
|
|
||
| ```agda | ||
| infinity-ℕ∞ : ℕ∞ | ||
| decons-ℕ∞ infinity-ℕ∞ = unit-Maybe infinity-ℕ∞ | ||
| ``` | ||
|
|
||
| ### The successor function on the conatural numbers | ||
|
|
||
| ```agda | ||
| succ-ℕ∞ : ℕ∞ → ℕ∞ | ||
| decons-ℕ∞ (succ-ℕ∞ x) = unit-Maybe x | ||
| ``` | ||
|
|
||
| ### The constructor function for conatural numbers | ||
|
|
||
| ```agda | ||
| cons-ℕ∞ : Maybe ℕ∞ → ℕ∞ | ||
| cons-ℕ∞ (inl x) = succ-ℕ∞ x | ||
| cons-ℕ∞ (inr x) = zero-ℕ∞ | ||
| ``` | ||
|
|
||
| ### Alternative definition of the deconstructor function for conatural numbers | ||
|
|
||
| ```agda | ||
| decons-ℕ∞' : ℕ∞ → Maybe ℕ∞ | ||
| decons-ℕ∞' x = rec-coproduct inl inr (decons-ℕ∞ x) | ||
|
|
||
| compute-decons-ℕ∞ : decons-ℕ∞' ~ decons-ℕ∞ | ||
| compute-decons-ℕ∞ x with decons-ℕ∞ x | ||
| compute-decons-ℕ∞ x | inl q = refl | ||
| compute-decons-ℕ∞ x | inr q = refl | ||
| ``` | ||
|
|
||
| ### The coiterator function for conatural numbers | ||
|
|
||
| ```agda | ||
| coit-ℕ∞ : {l : Level} {A : UU l} → (A → Maybe A) → A → ℕ∞ | ||
| decons-ℕ∞ (coit-ℕ∞ f x) with f x | ||
| decons-ℕ∞ (coit-ℕ∞ f x) | inl a = unit-Maybe (coit-ℕ∞ f a) | ||
| decons-ℕ∞ (coit-ℕ∞ f x) | inr _ = exception-Maybe | ||
| ``` | ||
|
|
||
| ### The corecursor function for conatural numbers | ||
|
|
||
| ```agda | ||
| corec-ℕ∞ : {l : Level} {A : UU l} → (A → ℕ∞ + Maybe A) → A → ℕ∞ | ||
| decons-ℕ∞ (corec-ℕ∞ f x) with f x | ||
| decons-ℕ∞ (corec-ℕ∞ f x) | inl q = unit-Maybe q | ||
| decons-ℕ∞ (corec-ℕ∞ f x) | inr (inl a) = unit-Maybe (corec-ℕ∞ f a) | ||
| decons-ℕ∞ (corec-ℕ∞ f x) | inr (inr *) = inr * | ||
| ``` | ||
|
|
||
| ## Properties | ||
|
|
||
| ### Zero is not a successor | ||
|
|
||
| ```agda | ||
| neq-zero-succ-ℕ∞ : (x : ℕ∞) → succ-ℕ∞ x ≠ zero-ℕ∞ | ||
| neq-zero-succ-ℕ∞ x p = is-not-exception-unit-Maybe x (ap decons-ℕ∞ p) | ||
| ``` | ||
|
|
||
| ### Zero is not the point at infinity | ||
|
|
||
| ```agda | ||
| neq-zero-infinity-ℕ∞ : infinity-ℕ∞ ≠ zero-ℕ∞ | ||
| neq-zero-infinity-ℕ∞ p = | ||
| is-not-exception-unit-Maybe infinity-ℕ∞ (ap decons-ℕ∞ p) | ||
|
|
||
| neq-infinity-zero-ℕ∞ : zero-ℕ∞ ≠ infinity-ℕ∞ | ||
| neq-infinity-zero-ℕ∞ = | ||
| is-symmetric-nonequal infinity-ℕ∞ zero-ℕ∞ neq-zero-infinity-ℕ∞ | ||
| ``` | ||
|
|
||
| ### The constructor function is a section of the deconstructor | ||
|
|
||
| ```agda | ||
| is-section-cons-ℕ∞ : is-section decons-ℕ∞ cons-ℕ∞ | ||
| is-section-cons-ℕ∞ (inl x) = refl | ||
| is-section-cons-ℕ∞ (inr x) = refl | ||
|
|
||
| section-decons-ℕ∞ : section decons-ℕ∞ | ||
| section-decons-ℕ∞ = cons-ℕ∞ , is-section-cons-ℕ∞ | ||
|
|
||
| retraction-cons-ℕ∞ : retraction cons-ℕ∞ | ||
| retraction-cons-ℕ∞ = decons-ℕ∞ , is-section-cons-ℕ∞ | ||
|
|
||
| is-injective-cons-ℕ∞ : is-injective cons-ℕ∞ | ||
| is-injective-cons-ℕ∞ = is-injective-retraction cons-ℕ∞ retraction-cons-ℕ∞ | ||
| ``` | ||
|
|
||
| ```agda | ||
| is-section-cons-ℕ∞' : is-section decons-ℕ∞' cons-ℕ∞ | ||
| is-section-cons-ℕ∞' (inl x) = refl | ||
| is-section-cons-ℕ∞' (inr x) = refl | ||
|
|
||
| section-decons-ℕ∞' : section decons-ℕ∞' | ||
| section-decons-ℕ∞' = cons-ℕ∞ , is-section-cons-ℕ∞' | ||
|
|
||
| retraction-cons-ℕ∞' : retraction cons-ℕ∞ | ||
| retraction-cons-ℕ∞' = decons-ℕ∞' , is-section-cons-ℕ∞' | ||
| ``` | ||
|
|
||
| ### The successor function is injective | ||
|
|
||
| ```agda | ||
| is-injective-succ-ℕ∞ : is-injective succ-ℕ∞ | ||
| is-injective-succ-ℕ∞ p = is-injective-inl (is-injective-cons-ℕ∞ p) | ||
| ``` | ||
|
|
||
| ## External links | ||
|
|
||
| - [CoNaturals](https://martinescardo.github.io/TypeTopology/CoNaturals.index.html) | ||
| at TypeTopology | ||
| - [extended natural numbers](https://ncatlab.org/nlab/show/extended+natural+number) | ||
| at $n$Lab |
82 changes: 82 additions & 0 deletions
82
src/elementary-number-theory/inclusion-natural-numbers-conatural-numbers.lagda.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,82 @@ | ||
| # The inclusion of the natural numbers into the conatural numbers | ||
|
|
||
| ```agda | ||
| {-# OPTIONS --guardedness #-} | ||
|
|
||
| module elementary-number-theory.inclusion-natural-numbers-conatural-numbers where | ||
| ``` | ||
|
|
||
| <details><summary>Imports</summary> | ||
|
|
||
| ```agda | ||
| open import elementary-number-theory.conatural-numbers | ||
| open import elementary-number-theory.infinite-conatural-numbers | ||
| open import elementary-number-theory.natural-numbers | ||
|
|
||
| open import foundation.action-on-identifications-functions | ||
| open import foundation.existential-quantification | ||
| open import foundation.injective-maps | ||
| open import foundation.negated-equality | ||
| open import foundation.negation | ||
| open import foundation.surjective-maps | ||
|
|
||
| open import foundation-core.empty-types | ||
| open import foundation-core.identity-types | ||
| ``` | ||
|
|
||
| </details> | ||
|
|
||
| ## Idea | ||
|
|
||
| The | ||
| {{#concept "inclusion of the nautural numbers into the conatural numbers" Agda=ℕ∞}} | ||
| is the inductively defined map | ||
|
|
||
| ```text | ||
| conatural-ℕ : ℕ → ℕ∞ | ||
| ``` | ||
|
|
||
| that sends zero to zero, and the successor of a natural number to the successor | ||
| of its inclusion. | ||
|
|
||
| ## Definitions | ||
|
|
||
| ### The canonical inclusion of the natural numbers into the conatural numbers | ||
|
|
||
| ```agda | ||
| conatural-ℕ : ℕ → ℕ∞ | ||
| conatural-ℕ zero-ℕ = zero-ℕ∞ | ||
| conatural-ℕ (succ-ℕ x) = succ-ℕ∞ (conatural-ℕ x) | ||
| ``` | ||
|
|
||
| ## Properties | ||
|
|
||
| ### The canonical inclusion of the natural numbers is injective | ||
|
|
||
| ```agda | ||
| is-injective-conatural-ℕ : is-injective conatural-ℕ | ||
| is-injective-conatural-ℕ {zero-ℕ} {zero-ℕ} p = refl | ||
| is-injective-conatural-ℕ {zero-ℕ} {succ-ℕ y} p = | ||
| ex-falso (neq-zero-succ-ℕ∞ (conatural-ℕ y) (inv p)) | ||
| is-injective-conatural-ℕ {succ-ℕ x} {zero-ℕ} p = | ||
| ex-falso (neq-zero-succ-ℕ∞ (conatural-ℕ x) p) | ||
| is-injective-conatural-ℕ {succ-ℕ x} {succ-ℕ y} p = | ||
| ap succ-ℕ (is-injective-conatural-ℕ {x} {y} (is-injective-succ-ℕ∞ p)) | ||
| ``` | ||
|
|
||
| ### The canonical inclusion of the natural numbers is not surjective | ||
|
|
||
| The canonical inclusion of the natural numbers is not surjective because it does | ||
| not hit the point at infinity. | ||
|
|
||
| ```text | ||
| neq-infinity-conatural-ℕ : (n : ℕ) → conatural-ℕ n ≠ infinity-ℕ∞ | ||
| neq-infinity-conatural-ℕ zero-ℕ = neq-infinity-zero-ℕ∞ | ||
| neq-infinity-conatural-ℕ (succ-ℕ n) p = | ||
| neq-infinity-conatural-ℕ n | ||
| ( is-injective-succ-ℕ∞ (p ∙ {! is-infinite-successor-condition-infinity-ℕ∞ !})) | ||
|
|
||
| is-not-surjective-conatural-ℕ : ¬ (is-surjective conatural-ℕ) | ||
| is-not-surjective-conatural-ℕ H = | ||
| elim-exists empty-Prop neq-infinity-conatural-ℕ (H infinity-ℕ∞) | ||
| ``` |
Oops, something went wrong.