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
    β„€-is-set : is-set β„€
    point  : β„€
    rotate : β„€ ≃ β„€

We start by giving Z{\mathbb{Z}} a mapping-out property: If XX is any other type with p:Xp : X and e:X≃Xe : X \simeq X, then there is a map Zβ†’X{\mathbb{Z}} \to X which sends our point (which may as well be called zero) to pp, 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
      : βˆ€ {β„“} {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.

      : βˆ€ {β„“} {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 nn is an integer expressed as a formal difference of naturals xβˆ’yx - y, then we can compute the power fn:X≃Xf^n : X \simeq X as the difference of equivalences (fy)βˆ’1∘fx(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

      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 (fy)βˆ’1∘fβˆ’1f∘fx(f^y)^{-1} \circ f^{-1}f \circ f^x is (fy)βˆ’1∘fx(f^y)^{-1} \circ f^x, which follows almost immediately from the properties of equivalences, cancelling the fβˆ’1ff^{-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 = rot int .fst point
  r .map-out-point p _ = refl
  r .map-out-rotate p rot i = rot i _

Using elimination by sign, we can divide the proof of uniqueness to the case where nn is a positive natural number, where nn is a negated natural number, and when nn is zero. The case n=0n = 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-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 = 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