open import 1Lab.HLevel.Retracts
open import 1Lab.Path.Groupoid
open import 1Lab.HLevel.Sets
open import 1Lab.Univalence
open import 1Lab.Type.Dec
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.Nat

module Data.Int where

Integers🔗

The integers are what you get when you complete the additive monoid structure on the naturals into a group. In non-cubical Agda, a representation of the integers as a coproduct $\bb{N} \coprod \bb{N}$ with one of the factors offset (to avoid having two zeroes) is adopted. In Cubical Agda we can adopt a representation much closer to a “classical” construction of the integers:

data Int : Type where
  diff : (x y : Nat) → Int
  quot : (m n : Nat) → diff m n ≡ diff (suc m) (suc n)

This is an alternative representation of the construction of integers as pairs $(x , y)\colon \bb{N}^2$ where $(a,b) = (c, d)$ iff $a + d = b + c$: An integer is an equivalence class of pairs of naturals, where $(a, b)$ is identified with $(1 + a, 1 + b)$, or, more type-theoretically, the integers are generated by the constructor diff which embeds a pair of naturals, and the path constructor quot which expresses that $(a, b)$ = $(1 + a, 1 + b)$.

This single generating path is enough to recover the “classical” quotient, which we do in steps. First, we… prove that that $n - n$ is $0$:

zeroes : (n : Nat) → diff   ≡ diff n n
zeroes zero = refl
zeroes (suc n) = zeroes n ∙ quot _ _

Additionally, offsetting a difference by a fixed natural, as long as it’s done on both sides of the difference, does not change which integer is being represented: That is, considering all three naturals as integers, $(a - b) = (n + a) - (n + b)$.

cancel : (a b n : Nat) → diff a b ≡ diff (n + a) (n + b)
cancel a b zero = refl
cancel a b (suc n) = cancel a b n ∙ quot _ _

As a final pair of helper lemmas, we find that if $n$ and $k$ differ by an absolute value of $b$, then the values $n - k$ and $b$ are the same (as long as we fix the sign — hence the two lemmas). The generic situation of “differing by $b$” is captured by fixing a natural number $a$ and adding $b$, because we have $(a + b) - a = b$ and $a - (a + b) = -b$.

offset-negative : (a b : Nat) → diff a (a + b) ≡ diff  b
offset-negative zero b = refl
offset-negative (suc a) b =
  diff (suc a) (suc (a + b)) ≡⟨ sym (quot _ _) ⟩≡
  diff a (a + b)             ≡⟨ offset-negative a b ⟩≡
  diff  b                   ∎

offset-positive : (a b : Nat) → diff (a + b) a ≡ diff b 
offset-positive zero b = refl
offset-positive (suc a) b =
  diff (suc (a + b)) (suc a) ≡⟨ sym (quot _ _) ⟩≡
  diff (a + b) a             ≡⟨ offset-positive a b ⟩≡
  diff b                    ∎

Those two are the last two lemmas we need to prove the “if” direction of “naturals are identified in the quotient iff they represent the same difference”: the construction same-difference below packages everything together with a bow on the top.

same-difference : {a b c d : Nat} → a + d ≡ b + c → diff a b ≡ diff c d
same-difference {zero} {b} {c} {d} path =
  sym ( diff c d       ≡⟨ ap₂ diff refl path ⟩≡
        diff c (b + c) ≡⟨ ap₂ diff refl (+-commutative b c) ⟩≡
        diff c (c + b) ≡⟨ offset-negative _ _ ⟩≡
        diff  b       ∎
      )
same-difference {suc a} {zero} {c} {d} path =
  sym ( diff c d             ≡⟨ ap₂ diff (sym path) refl ⟩≡
        diff (suc a + d) d   ≡⟨ ap₂ diff (+-commutative (suc a) d) refl ⟩≡
        diff (d + suc a) d   ≡⟨ offset-positive _ _ ⟩≡
        diff (suc a)        ∎
      )
same-difference {suc a} {suc b} {c} {d} path =
  diff (suc a) (suc b) ≡⟨ sym (quot _ _) ⟩≡
  diff a b             ≡⟨ same-difference (suc-inj path) ⟩≡
  diff c d             ∎

In the other direction, we must be clever: we use path induction, defining a type family $\id{Code}_{a,b}(x)$ such that the fibre of $\id{Code}_{a,b}$ over $(c, d)$ is $a + d = b + c$. We can then use path induction to construct the map inverse to same-difference. On the way, the first thing we establish is a pair of observations about equalities on the natural numbers: $a + n = b + m$ and $a + 1 + n = b + 1 + m$ are equivalent conditions. This can be seen by commutativity and injectivity of the successor function, but below we prove it using equational reasoning, without appealing to commutativity.

module ℤ-Path where
  private
    variable a b m n c d : Nat
  encode-p-from : (a + n ≡ b + m) → (a + suc n ≡ b + suc m)
  encode-p-from {a = a} {n} {b} {m} p =
    a + suc n   ≡⟨ +-sucr a n ⟩≡
    suc (a + n) ≡⟨ ap suc p ⟩≡
    suc (b + m) ≡˘⟨ +-sucr b m ⟩≡˘
    b + suc m   ∎

  encode-p-to : (a + suc n ≡ b + suc m) → (a + n ≡ b + m)
  encode-p-to {a} {n} {b} {m} p = suc-inj (sym (+-sucr a n) ∙ p ∙ +-sucr b m)

We then define, fixing two natural numbers $a, b$, the family $\id{Code}_{a,b}(x)$ by recursion on the integer $x$. Recall that we want the fibre over $\id{diff}(c, d)$ to be $a + d = b + c$, so that’s our pick. Now, the quot path constructor mandates that the fibre over $(c, d)$ be the same as that over $(1 + c, 1 + d)$ — but this follows by propositional extensionality and the pair of observations above.

  Code : ∀ (a b : Nat) (x : Int) → Type
  Code a b (diff c d) = a + d ≡ b + c
  Code a b (quot m n i) = path i where
    path : (a + n ≡ b + m) ≡ (a + suc n ≡ b + suc m)
    path = ua (prop-ext (Nat-is-set _ _) (Nat-is-set _ _) encode-p-from encode-p-to)

Hence, if we have a path $\id{diff}(a, b) = x$, we can apply path induction, whence it suffices to consider the case where $x$ is literally_ the difference of $a$ and $b$. To lift this into our Code fibration, we must show that $a + b = b + a$, but this is exactly commutativity of addition on $\bb{N}$.

  encode : ∀ (a b : Nat) (x : Int) → diff a b ≡ x → Code a b x
  encode a b x = J (λ x p → Code a b x) (+-commutative a b)

As a finishing touch, we give Int instances for Number and Negative, meaning that we can use positive and negative integer literals to denote values of Int.

instance
  Number-Int : Number Int
  Number-Int .Number.Constraint _ = ⊤
  Number-Int .Number.fromNat n = diff n 

  Negative-Int : Negative Int
  Negative-Int .Negative.Constraint _ = ⊤
  Negative-Int .Negative.fromNeg n = diff  n

h-level🔗

To prove that Int is a set, we prove that it is equivalent to an inductive (rather than higher-inductive) representation of the integers. Since this latter representation (which we call Int') has decidable equality, it is a set.

module _ where
  open import Data.Int.Inductive
    renaming ( Int to Int'
             ; Discrete-Int to Discrete-Int'
             )

There is a canonical map which takes pairs of naturals to their difference as an Int', which is ℕ-; It can be shown that this map extends to a function from Int, since it respects the generating equation quot definitionally:

  private
    to-inductive : Int → Int'
    to-inductive (diff x y) = x ℕ- y
    to-inductive (quot m n i) = m ℕ- n

    from-inductive : Int' → Int
    from-inductive (pos x) = diff x 
    from-inductive (negsuc x) = diff  ( + x)

Mapping from Int' to Int sends the positive numbers to $(x, 0)$ and the negative numbers to $(0, x)$. Note that the left summand (the “negative numbers”) in the inductive definition of Int' are offset by one; Hence, the mapping out of negsuc sends $x$ (which really represents the number $-(1+x)$) to… well, $-(1 + x)$.

Using the helpers quot-triangle and quot-diamond, we construct an inductive proof that the integers are a retract of Agda’s built-in Int' type; Since the latter is a set, then so is ours!

    to-from-inductive : (x : Int) → from-inductive (to-inductive x) ≡ x
    to-from-inductive (diff x zero)            = refl
    to-from-inductive (diff zero (suc y))      = refl
    to-from-inductive (diff (suc x) (suc y))   = to-from-inductive (diff x y) ∙ quot _ _

    to-from-inductive (quot m zero i)          = quot-triangle _ _ i
    to-from-inductive (quot zero (suc n) i)    = quot-triangle _ _ i
    to-from-inductive (quot (suc m) (suc n) i) =
      to-from-inductive (quot _ _ i) ∙ quot-diamond _ _ i

  Int-is-set : is-set Int
  Int-is-set = retract→is-hlevel  from-inductive to-inductive to-from-inductive
    (Discrete→is-set Discrete-Int')

Recursion🔗

If we want to define a map $f : \bb{Z} \to X$, it suffices to give a function $f : \bb{N}^2 \to X$ which respects the quotient, in the following sense:

Int-rec : ∀ {ℓ} {X : Type ℓ}
        → (f : Nat → Nat → X)
        → (q : (a b : _) → f a b ≡ f (suc a) (suc b))
        → Int → X
Int-rec f q (diff x y) = f x y
Int-rec f q (quot m n i) = q m n i

However, since $X$ can be a more general space, not necessarily a set, defining a binary operation $f' : \bb{Z}^2 \to X$ can be quite involved! It doesn’t suffice to exhibit a function from $\bb{N}^4$ which respects the quotient separately in each argument:

Int-rec₂ : ∀ {ℓ} {B : Type ℓ}
         → (f : Nat × Nat → Nat × Nat → B)
         → (pl     : (a b x y : _) → f (a , b) (x , y) ≡ f (suc a , suc b) (x , y))
         → (pr     : (a b x y : _) → f (a , b) (x , y) ≡ f (a , b) (suc x , suc y))

In addition, we must have that these two paths pl and pr are coherent. There are two ways of obtaining an equality $f(a, b, x, y) = f(\id{S}a,\id{S}b,\id{S}x,\id{S}y)$ (pl after pr and pr after pl, respectively) and these must be homotopic:

         → (square : (a b x y : _) →
              Square (pl a b x y) (pr a b x y)
                     (pr (suc a) (suc b) x y)
                     (pl a b (suc x) (suc y)))
         → Int → Int → B

The type of square says that we need the following square of paths to commute, which says exactly that pl ∙ pr and pr ∙ pl are homotopic and imposes no further structure on $X$¹:

Int-rec₂ f p-l p-r sq (diff a b) (diff x y)     = f (a , b) (x , y)
Int-rec₂ f p-l p-r sq (diff a b) (quot x y i)   = p-r a b x y i
Int-rec₂ f p-l p-r sq (quot a b i) (diff x y)   = p-l a b x y i
Int-rec₂ f p-l p-r sq (quot a b i) (quot x y j) = sq a b x y i j

However, when the type $X$ we are mapping into is a set, as is the case for the integers themselves, the square is automatically satisfied, so we can give a simplified recursion principle:

Int-rec₂-set :
  ∀ {ℓ} {B : Type ℓ}
  → is-set B
  → (f : Nat × Nat → Nat × Nat → B)
  → (pl     : (a b x y : _) → f (a , b) (x , y) ≡ f (suc a , suc b) (x , y))
  → (pr     : (a b x y : _) → f (a , b) (x , y) ≡ f (a , b) (suc x , suc y))
  → Int → Int → B
Int-rec₂-set iss-b f pl pr = Int-rec₂ f pl pr square where
  square : (a b x y : _) → _
  square a b x y = is-set→squarep (λ i j → iss-b) _ _ _ _

Furthermore, when proving propositions of the integers, the quotient is automatically respected, so it suffices to give the case for diff:

Int-elim-prop : ∀ {ℓ} {P : Int → Type ℓ}
              → ((x : Int) → is-prop (P x))
              → (f : (a b : Nat) → P (diff a b))
              → (x : Int) → P x
Int-elim-prop pprop f (diff a b) = f a b
Int-elim-prop pprop f (quot m n i) =
  is-prop→pathp (λ i → pprop (quot m n i)) (f m n) (f (suc m) (suc n)) i

Int-elim₂-prop : ∀ {ℓ} {P : Int → Int → Type ℓ}
               → ((x y : Int) → is-prop (P x y))
               → (f : (a b x y : Nat) → P (diff a b) (diff x y))
               → (x : Int) (y : Int) → P x y
Int-elim₂-prop pprop f =
  Int-elim-prop (λ x → Π-is-hlevel  (pprop x))
    λ a b int → Int-elim-prop (λ x → pprop (diff a b) x) (f a b) int

Int-elim₃-prop : ∀ {ℓ} {P : Int → Int → Int → Type ℓ}
               → ((x y z : Int) → is-prop (P x y z))
               → (f : (a b c d e f : Nat) → P (diff a b) (diff c d) (diff e f))
               → (x : Int) (y : Int) (z : Int) → P x y z
Int-elim₃-prop pprop f =
  Int-elim₂-prop (λ x y → Π-is-hlevel  (pprop x y))
    λ a b c d int → Int-elim-prop (λ x → pprop (diff a b) (diff c d) x)
                                  (f a b c d)
                                  int

Algebra🔗

With these recursion and elimination helpers, it becomes routine to lift the algebraic operations from naturals to integers:

Successors🔗

The simplest “algebraic operation” on an integer is taking its successor. In fact, the integers are characterised by being the free type with an equivalence - that equivalence being “successor”.

sucℤ : Int → Int
sucℤ (diff x y) = diff (suc x) y
sucℤ (quot m n i) = quot (suc m) n i

predℤ : Int → Int
predℤ (diff x y) = diff x (suc y)
predℤ (quot m n i) = quot m (suc n) i

The successor of $(a, b)$ is $(1 + a, b)$. Similarly, the predecessor of $(a, b)$ is $(a, 1 + b)$. By the generating equality quot, we have that predecessor and successor are inverses, since applying both (in either order) takes $(a, b)$ to $(1 + a, 1 + b)$.

pred-sucℤ : (x : Int) → predℤ (sucℤ x) ≡ x
pred-sucℤ (diff x y) = sym (quot x y)
pred-sucℤ (quot m n i) j = quot-diamond m n i (~ j)

suc-predℤ : (x : Int) → sucℤ (predℤ x) ≡ x
suc-predℤ (diff x y) = sym (quot x y)
suc-predℤ (quot m n i) j = quot-diamond m n i (~ j)

sucℤ-is-equiv : is-equiv sucℤ
sucℤ-is-equiv = is-iso→is-equiv (iso predℤ suc-predℤ pred-sucℤ)

predℤ-is-equiv : is-equiv predℤ
predℤ-is-equiv = is-iso→is-equiv (iso sucℤ pred-sucℤ suc-predℤ)

Addition🔗

_+ℤ_ : Int → Int → Int
_+ℤ_ =
  Int-rec₂-set
    Int-is-set
    (λ { (a , b) (c , d) → diff (a + c) (b + d)})
    (λ a b x y → quot _ _)
    (λ a b x y → quot _ _ ∙ ap₂ diff (sym (+-sucr _ _)) (sym (+-sucr _ _)))

Since addition of integers is (essentially!) addition of pairs of naturals, the algebraic properties of + on the natural numbers automatically lift to properties about _+ℤ_, using the recursion helpers for props (Int-elim-prop) and the fact that equality of integers is a proposition.

+ℤ-associative : (x y z : Int) → (x +ℤ y) +ℤ z ≡ x +ℤ (y +ℤ z)
+ℤ-associative =
  Int-elim₃-prop
    (λ x y z → Int-is-set _ _)
    (λ a b c d e f → ap₂ diff (+-associative a c e) (+-associative b d f))

+ℤ-zerol : (x : Int) →  +ℤ x ≡ x
+ℤ-zerol = Int-elim-prop (λ x → Int-is-set _ _) (λ a b → refl)

+ℤ-zeror : (x : Int) → x +ℤ  ≡ x
+ℤ-zeror =
  Int-elim-prop (λ x → Int-is-set _ _) (λ a b → ap₂ diff (+-zeror a) (+-zeror b))

+ℤ-commutative : (x y : Int) → x +ℤ y ≡ y +ℤ x
+ℤ-commutative =
  Int-elim₂-prop (λ x y → Int-is-set _ _)
    (λ a b c d → ap₂ diff (+-commutative a c) (+-commutative b d))

Inverses🔗

Every integer $x$ has an additive inverse, denoted $-x$, which is obtained by swapping the components of the pair. Since the definition of negate is very simple, it can be written conveniently without using Int-rec:

negate : Int → Int
negate (diff x y) = diff y x
negate (quot m n i) = quot n m i

The proof that $-x$ is an additive inverse to $x$ follows, essentially, from commutativity of addition on natural numbers, and the fact that all zeroes are identified.

+ℤ-inverser : (x : Int) → x +ℤ negate x ≡ 
+ℤ-inverser =
  Int-elim-prop (λ _ → Int-is-set _ _) λ where
    a b → diff (a + b) (b + a) ≡⟨ ap₂ diff refl (+-commutative b a) ⟩≡
          diff (a + b) (a + b) ≡⟨ sym (zeroes (a + b)) ⟩≡
          diff               ∎

+ℤ-inversel : (x : Int) → negate x +ℤ x ≡ 
+ℤ-inversel =
  Int-elim-prop (λ _ → Int-is-set _ _) λ where
    a b → diff (b + a) (a + b) ≡⟨ ap₂ diff (+-commutative b a) refl ⟩≡
          diff (a + b) (a + b) ≡⟨ sym (zeroes (a + b)) ⟩≡
          diff               ∎

Since negate is precisely what’s missing for Nat to be a group, we can turn the integers into a group. Subtraction is defined as addition with the inverse, rather than directly on diff:

_-ℤ_ : Int → Int → Int
x -ℤ y = x +ℤ negate y