# The universal property of the integers

Content created by Fredrik Bakke, Egbert Rijke and Vojtěch Štěpančík.

Created on 2023-08-28.

module elementary-number-theory.universal-property-integers where

Imports
open import elementary-number-theory.integers
open import elementary-number-theory.natural-numbers

open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.propositions
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels


## Idea

The universal property of the integers states that given any type X equipped with a point x : X and an automorphism e : X ≃ X, there is a unique structure preserving map from ℤ to X.

abstract
elim-ℤ :
{ l1 : Level} (P : ℤ → UU l1)
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
( k : ℤ) → P k
elim-ℤ P p0 pS (inl zero-ℕ) =
map-inv-is-equiv (is-equiv-map-equiv (pS neg-one-ℤ)) p0
elim-ℤ P p0 pS (inl (succ-ℕ x)) =
map-inv-is-equiv
( is-equiv-map-equiv (pS (inl (succ-ℕ x))))
( elim-ℤ P p0 pS (inl x))
elim-ℤ P p0 pS (inr (inl _)) = p0
elim-ℤ P p0 pS (inr (inr zero-ℕ)) = map-equiv (pS zero-ℤ) p0
elim-ℤ P p0 pS (inr (inr (succ-ℕ x))) =
map-equiv
( pS (inr (inr x)))
( elim-ℤ P p0 pS (inr (inr x)))

compute-zero-elim-ℤ :
{ l1 : Level} (P : ℤ → UU l1)
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
Id (elim-ℤ P p0 pS zero-ℤ) p0
compute-zero-elim-ℤ P p0 pS = refl

compute-succ-elim-ℤ :
{ l1 : Level} (P : ℤ → UU l1)
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) (k : ℤ) →
Id (elim-ℤ P p0 pS (succ-ℤ k)) (map-equiv (pS k) (elim-ℤ P p0 pS k))
compute-succ-elim-ℤ P p0 pS (inl zero-ℕ) =
inv
( is-section-map-inv-is-equiv
( is-equiv-map-equiv (pS (inl zero-ℕ)))
( elim-ℤ P p0 pS (succ-ℤ (inl zero-ℕ))))
compute-succ-elim-ℤ P p0 pS (inl (succ-ℕ x)) =
inv
( is-section-map-inv-is-equiv
( is-equiv-map-equiv (pS (inl (succ-ℕ x))))
( elim-ℤ P p0 pS (succ-ℤ (inl (succ-ℕ x)))))
compute-succ-elim-ℤ P p0 pS (inr (inl _)) = refl
compute-succ-elim-ℤ P p0 pS (inr (inr _)) = refl

ELIM-ℤ :
{ l1 : Level} (P : ℤ → UU l1)
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) → UU l1
ELIM-ℤ P p0 pS =
Σ ( (k : ℤ) → P k)
( λ f →
( ( Id (f zero-ℤ) p0) ×
( (k : ℤ) → Id (f (succ-ℤ k)) ((map-equiv (pS k)) (f k)))))

Elim-ℤ :
{ l1 : Level} (P : ℤ → UU l1)
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) → ELIM-ℤ P p0 pS
pr1 (Elim-ℤ P p0 pS) = elim-ℤ P p0 pS
pr1 (pr2 (Elim-ℤ P p0 pS)) = compute-zero-elim-ℤ P p0 pS
pr2 (pr2 (Elim-ℤ P p0 pS)) = compute-succ-elim-ℤ P p0 pS

equiv-comparison-map-Eq-ELIM-ℤ :
{ l1 : Level} (P : ℤ → UU l1)
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
( s t : ELIM-ℤ P p0 pS) (k : ℤ) →
Id ((pr1 s) k) ((pr1 t) k) ≃ Id ((pr1 s) (succ-ℤ k)) ((pr1 t) (succ-ℤ k))
equiv-comparison-map-Eq-ELIM-ℤ P p0 pS s t k =
( ( equiv-concat (pr2 (pr2 s) k) (pr1 t (succ-ℤ k))) ∘e
( equiv-concat' (map-equiv (pS k) (pr1 s k)) (inv (pr2 (pr2 t) k)))) ∘e
( equiv-ap (pS k) (pr1 s k) (pr1 t k))

zero-Eq-ELIM-ℤ :
{ l1 : Level} (P : ℤ → UU l1)
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
( s t : ELIM-ℤ P p0 pS) (H : (pr1 s) ~ (pr1 t)) → UU l1
zero-Eq-ELIM-ℤ P p0 pS s t H =
Id (H zero-ℤ) ((pr1 (pr2 s)) ∙ (inv (pr1 (pr2 t))))

succ-Eq-ELIM-ℤ :
{ l1 : Level} (P : ℤ → UU l1)
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
( s t : ELIM-ℤ P p0 pS) (H : (pr1 s) ~ (pr1 t)) → UU l1
succ-Eq-ELIM-ℤ P p0 pS s t H =
( k : ℤ) →
Id
( H (succ-ℤ k))
( map-equiv (equiv-comparison-map-Eq-ELIM-ℤ P p0 pS s t k) (H k))

Eq-ELIM-ℤ :
{ l1 : Level} (P : ℤ → UU l1)
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
( s t : ELIM-ℤ P p0 pS) → UU l1
Eq-ELIM-ℤ P p0 pS s t =
ELIM-ℤ
( λ k → Id (pr1 s k) (pr1 t k))
( (pr1 (pr2 s)) ∙ (inv (pr1 (pr2 t))))
( equiv-comparison-map-Eq-ELIM-ℤ P p0 pS s t)

reflexive-Eq-ELIM-ℤ :
{ l1 : Level} (P : ℤ → UU l1)
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
( s : ELIM-ℤ P p0 pS) → Eq-ELIM-ℤ P p0 pS s s
pr1 (reflexive-Eq-ELIM-ℤ P p0 pS (f , p , H)) = refl-htpy
pr1 (pr2 (reflexive-Eq-ELIM-ℤ P p0 pS (f , p , H))) = inv (right-inv p)
pr2 (pr2 (reflexive-Eq-ELIM-ℤ P p0 pS (f , p , H))) = inv ∘ (right-inv ∘ H)

Eq-ELIM-ℤ-eq :
{ l1 : Level} (P : ℤ → UU l1) →
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
( s t : ELIM-ℤ P p0 pS) → Id s t → Eq-ELIM-ℤ P p0 pS s t
Eq-ELIM-ℤ-eq P p0 pS s .s refl = reflexive-Eq-ELIM-ℤ P p0 pS s

abstract
is-torsorial-Eq-ELIM-ℤ :
{ l1 : Level} (P : ℤ → UU l1) →
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
( s : ELIM-ℤ P p0 pS) → is-torsorial (Eq-ELIM-ℤ P p0 pS s)
is-torsorial-Eq-ELIM-ℤ P p0 pS s =
is-torsorial-Eq-structure
( is-torsorial-htpy (pr1 s))
( pair (pr1 s) refl-htpy)
( is-torsorial-Eq-structure
( is-contr-is-equiv'
( Σ (Id (pr1 s zero-ℤ) p0) (λ α → Id α (pr1 (pr2 s))))
( tot (λ α → right-transpose-eq-concat refl α (pr1 (pr2 s))))
( is-equiv-tot-is-fiberwise-equiv
( λ α → is-equiv-right-transpose-eq-concat refl α (pr1 (pr2 s))))
( is-torsorial-Id' (pr1 (pr2 s))))
( pair (pr1 (pr2 s)) (inv (right-inv (pr1 (pr2 s)))))
( is-contr-is-equiv'
( Σ ( ( k : ℤ) → Id (pr1 s (succ-ℤ k)) (pr1 (pS k) (pr1 s k)))
( λ β → β ~ (pr2 (pr2 s))))
( tot (λ β → right-transpose-htpy-concat refl-htpy β (pr2 (pr2 s))))
( is-equiv-tot-is-fiberwise-equiv
( λ β →
is-equiv-right-transpose-htpy-concat refl-htpy β (pr2 (pr2 s))))
( is-torsorial-htpy' (pr2 (pr2 s)))))

abstract
is-equiv-Eq-ELIM-ℤ-eq :
{ l1 : Level} (P : ℤ → UU l1) →
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
( s t : ELIM-ℤ P p0 pS) → is-equiv (Eq-ELIM-ℤ-eq P p0 pS s t)
is-equiv-Eq-ELIM-ℤ-eq P p0 pS s =
fundamental-theorem-id
( is-torsorial-Eq-ELIM-ℤ P p0 pS s)
( Eq-ELIM-ℤ-eq P p0 pS s)

eq-Eq-ELIM-ℤ :
{ l1 : Level} (P : ℤ → UU l1) →
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
( s t : ELIM-ℤ P p0 pS) → Eq-ELIM-ℤ P p0 pS s t → Id s t
eq-Eq-ELIM-ℤ P p0 pS s t = map-inv-is-equiv (is-equiv-Eq-ELIM-ℤ-eq P p0 pS s t)

abstract
is-prop-ELIM-ℤ :
{ l1 : Level} (P : ℤ → UU l1) →
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
is-prop (ELIM-ℤ P p0 pS)
is-prop-ELIM-ℤ P p0 pS =
is-prop-all-elements-equal
( λ s t → eq-Eq-ELIM-ℤ P p0 pS s t
( Elim-ℤ
( λ k → Id (pr1 s k) (pr1 t k))
( (pr1 (pr2 s)) ∙ (inv (pr1 (pr2 t))))
( equiv-comparison-map-Eq-ELIM-ℤ P p0 pS s t)))


### The dependent universal property of the integers

abstract
is-contr-ELIM-ℤ :
{ l1 : Level} (P : ℤ → UU l1) →
( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
is-contr (ELIM-ℤ P p0 pS)
is-contr-ELIM-ℤ P p0 pS =
is-proof-irrelevant-is-prop (is-prop-ELIM-ℤ P p0 pS) (Elim-ℤ P p0 pS)


### The universal property of the integers

The nondependent universal property of the integers is a special case of the dependent universal property applied to constant type families.

ELIM-ℤ' :
{ l1 : Level} {X : UU l1} (x : X) (e : X ≃ X) → UU l1
ELIM-ℤ' {X = X} x e = ELIM-ℤ (λ k → X) x (λ k → e)

abstract
universal-property-ℤ :
{ l1 : Level} {X : UU l1} (x : X) (e : X ≃ X) → is-contr (ELIM-ℤ' x e)
universal-property-ℤ {X = X} x e = is-contr-ELIM-ℤ (λ k → X) x (λ k → e)