open import 1Lab.Prelude open import Data.Int import Data.Int.Inductive as Ind module Data.Int.Universal where

# Universal property of the integersπ

We define and prove a type-theoretic universal property of the integers, which characterises them as the initial pointed set equipped with an auto-equivalence, in much the same way that the natural numbers are characterised as being the initial pointed type equipped with an endomorphism.

record Integers (β€ : Type) : TypeΟ where no-eta-equality field β€-is-set : is-set β€ point : β€ rotate : β€ β β€

We start by giving
${\mathbb{Z}}$
a *mapping-out* property: If
$X$
is any other type with
$p : X$
and
$e : X \simeq X$,
then there is a map
${\mathbb{Z}} \to X$
which sends our point (which may as well be called *zero*) to
$p$,
and commutes with our equivalence. Note that commuting with the
equivalence implies commuting with its inverse, too.

map-out : β {β} {X : Type β} β X β X β X β β€ β X map-out-point : β {β} {X : Type β} (p : X) (r : X β X) β map-out p r point β‘ p map-out-rotate : β {β} {X : Type β} (p : X) (r : X β X) (i : β€) β map-out p r (rotate .fst i) β‘ r .fst (map-out p r i)

We obtain a sort of initiality by requiring that map-out be unique among functions with these properties.

map-out-unique : β {β} {X : Type β} (f : β€ β X) {p : X} {r : X β X} β f point β‘ p β (β x β f (rotate .fst x) β‘ r .fst (f x)) β β x β f x β‘ map-out p r x

We now prove that the integers are a set of integers. This isnβt as
tautological as it sounds, sadly, because our integers were designed to
be convenient for *algebra*, and this specific universal property
is rather divorced from algebra. Fortunately, itβs still not too hard,
so join me.

open Integers Int-integers : Integers Int Int-integers = r where module map-out {β} {X : Type β} (l : X β X) where

We start by making a simple observation: Exponentiation commutes with difference, where by exponentiation we mean iterated composition of equivalences. That is: if $n$ is an integer expressed as a formal difference of naturals $x - y$, then we can compute the power $f^n : X \simeq X$ as the difference of equivalences $(f^y)^{-1} \circ f^x$.

n-power : Nat β X β X n-power zero = (Ξ» x β x) , id-equiv n-power (suc x) = n-power x βe l private lemma : β m n x β (n-power n eβ»ΒΉ) .fst (n-power m .fst x) β‘ (n-power n eβ»ΒΉ) .fst (Equiv.from (l) (l .fst (n-power m .fst x))) lemma m n x = ap ((n-power n eβ»ΒΉ) .fst) (sym (Equiv.Ξ· l _)) map : Int β X β X map (diff x y) = n-power x βe (n-power y eβ»ΒΉ) map (quot m n i) = Ξ£-prop-path is-equiv-is-prop {x = n-power m βe (n-power n eβ»ΒΉ)} {y = n-power (suc m) βe (n-power (suc n) eβ»ΒΉ)} (funext (lemma m n)) i

To show that this computation respects the quotient, we must calculate that $(f^y)^{-1} \circ f^{-1}f \circ f^x$ is $(f^y)^{-1} \circ f^x$, which follows almost immediately from the properties of equivalences, cancelling the $f^{-1}f$ critical pair in the middle.

r : Integers Int r .β€-is-set = hlevel 2 r .point = 0 r .rotate = sucβ€ , sucβ€-is-equiv r .map-out point rot int = map-out.map rot int .fst point r .map-out-point p _ = refl r .map-out-rotate p rot i = map-out.map-suc rot i _

Using elimination by *sign*, we can divide the proof of
uniqueness to the case where
$n$
is a positive natural number, where
$n$
is a negated natural number, and when
$n$
is zero. The case
$n = 0$
is one of the assumptions, the other cases follow by induction (on
naturals).

r .map-out-unique {X = X} f {point} {rot} path htpy = Int-elim-by-sign (Ξ» z β f z β‘ r .map-out _ _ z) unique-pos unique-neg path where abstract unique-pos : β k β f (diff k 0) β‘ map-out.n-power rot k .fst point unique-pos zero = path unique-pos (suc k) = htpy (diff k 0) β ap (rot .fst) (unique-pos k) unique-neg : β k β f (diff 0 k) β‘ Equiv.from (map-out.n-power rot k) point unique-neg zero = path unique-neg (suc k) = sym (Equiv.Ξ· rot _) Β·Β· ap (Equiv.from rot) ( sym (htpy (diff 0 (suc k))) Β·Β· ap f (sym (quot 0 k)) Β·Β· unique-neg k) Β·Β· sym (map-out.negativesβ»ΒΉ rot k _)

## Inductive integers are integersπ

In the 1Lab, we have another implementation of the integers, in
addition to the ones defined by quotient, which we have already
characterised as satisfying the universal property, above. These are the
*inductive integers*: defined as a particular binary coproduct of
natural numbers. To avoid the problem of having βtwo zeroesβ, one of the
summands is tagged βnegative successor,β rather than βsuccessorβ, so
that `negsuc 0`

indicates the number
$-1$.

We have already proven that the inductive integers have a successor equivalence: What we now do is prove this equivalence is universal.

Inductive-integers : Integers Ind.Int Inductive-integers = r where module map-out {β} {X : Type β} (l : X β X) where pos : Nat β X β X pos zero = _ , id-equiv pos (suc x) = pos x βe l neg : Nat β X β X neg zero = l eβ»ΒΉ neg (suc x) = neg x βe (l eβ»ΒΉ) to : Ind.Int β X β X to (Ind.pos x) = pos x to (Ind.negsuc x) = neg x r : Integers Ind.Int r .β€-is-set = Discreteβis-set Ind.Discrete-Int r .point = Ind.pos 0 r .rotate = Ind.suc-equiv r .map-out p e i = map-out.to e i .fst p r .map-out-point p _ = refl r .map-out-rotate p e = go where go : β x β r .map-out p e (r .rotate .fst x) β‘ e .fst (r .map-out p e x) go (Ind.pos x) = refl go (Ind.negsuc zero) = sym (Equiv.Ξ΅ e _) go (Ind.negsuc (suc x)) = sym (Equiv.Ξ΅ e _) r .map-out-unique f {p} {rot} fz fr = go where pos : β n β f (Ind.pos n) β‘ map-out.pos rot n .fst p pos zero = fz pos (suc n) = fr (Ind.pos n) β ap (rot .fst) (pos n) map-pred : β n β f (Ind.pred-int n) β‘ Equiv.from rot (f n) map-pred n = sym (Equiv.Ξ· rot _) Β·Β· ap (Equiv.from rot) (sym (fr _)) Β·Β· ap (Equiv.from rot β f) (Ind.suc-pred n) neg : β n β f (Ind.negsuc n) β‘ map-out.neg rot n .fst p neg zero = map-pred (Ind.pos 0) β ap (Equiv.from rot) fz neg (suc n) = map-pred (Ind.negsuc n) β ap (Equiv.from rot) (neg n) go : β i β f i β‘ r .map-out _ _ i go (Ind.pos x) = pos x go (Ind.negsuc x) = neg x