open import 1Lab.Prelude

open import Data.Int hiding (pos ; neg)

import Data.Int.Base as Ind
import Data.Int.HIT as HIT

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 a mapping-out property: If is any other type with and then there is a map which sends our point (which may as well be called zero) to 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


By a standard categorical argument, existence and uniqueness together give us an induction principle for the integers: to construct a section of a type family it is enough to give an element of and a family of equivalences

  β€-Ξ· : β z β map-out point rotate z β‘ z
β€-Ξ· z = sym (map-out-unique id refl (Ξ» _ β refl) z)

induction
: β {β} {P : β€ β Type β}
β P point
β (β z β P z β P (rotate .fst z))
β β z β P z
induction {P = P} pp pr = section where
tot : β€ β Ξ£ β€ P
tot = map-out (point , pp) (Ξ£-ap rotate pr)

is-section : β z β tot z .fst β‘ map-out point rotate z
is-section = map-out-unique (fst β tot)
(ap fst (map-out-point _ _))
(Ξ» z β ap fst (map-out-rotate _ _ z))

section : β z β P z
section z = subst P (is-section z β β€-Ξ· z) (tot z .snd)

  map-out-rotate-inv
: β {β} {X : Type β} (p : X) (r : X β X) (i : β€)
β map-out p r (Equiv.from rotate i)
β‘ Equiv.from r (map-out p r i)
map-out-rotate-inv p r i =
sym (Equiv.Ξ· r _)
Β·Β· ap (Equiv.from r) (sym (map-out-rotate p r _))
Β·Β· ap (Equiv.from r β map-out p r) (Equiv.Ξ΅ rotate i)


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

HIT-Int-integers : Integers HIT.Int
HIT-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 is an integer expressed as a formal difference of naturals then we can compute the power as the difference of equivalences

    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 _))

go : HIT.Int β X β X
go (HIT.diff x y) = n-power x βe (n-power y eβ»ΒΉ)
go (HIT.quot m n i) = Ξ£-prop-path!
{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 is which follows almost immediately from the properties of equivalences, cancelling the critical pair in the middle.

    negatives   : β k x β Equiv.from (n-power k) (l .fst x) β‘ l .fst (Equiv.from (n-power k) x)
negativesβ»ΒΉ : β k x β Equiv.from (n-power k) (Equiv.from l x) β‘ Equiv.from l (Equiv.from (n-power k) x)

negatives zero x = refl
negatives (suc k) x =
ap (Equiv.from (n-power k)) (Equiv.Ξ· l x)
β sym (ap (l .fst) (negativesβ»ΒΉ k x) β Equiv.Ξ΅ l _)

negativesβ»ΒΉ zero x = refl
negativesβ»ΒΉ (suc k) x = negativesβ»ΒΉ k _

abstract
map-suc : β i x β go (HIT.sucβ€ i) .fst x β‘ l .fst (go i .fst x)
map-suc = HIT.Int-elim-by-sign
(Ξ» i β β x β go (HIT.sucβ€ i) .fst x β‘ l .fst (go i .fst x))
(Ξ» _ _ β refl)
negatives
(Ξ» _ β refl)

  r : Integers HIT.Int
r .β€-is-set = hlevel 2
r .point = 0
r .rotate = HIT.sucβ€ , HIT.sucβ€-is-equiv
r .map-out point rot int = map-out.go 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 is a positive natural number, where is a negated natural number, and when is zero. The case is one of the assumptions, the other cases follow by induction (on naturals).

  r .map-out-unique {X = X} f {point} {rot} path htpy =
HIT.Int-elim-by-sign (Ξ» z β f z β‘ r .map-out _ _ z) unique-pos unique-neg path
where abstract
unique-pos : β k β f (HIT.diff k 0) β‘ map-out.n-power rot k .fst point
unique-pos zero = path
unique-pos (suc k) = htpy (HIT.diff k 0) β ap (rot .fst) (unique-pos k)

unique-neg : β k β f (HIT.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 (HIT.diff 0 (suc k)))
Β·Β· ap f (sym (HIT.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

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

Int-integers : Integers Ind.Int
Int-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β€ 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