<!--
```agda
open import 1Lab.Prelude

open import Data.Nat.Solver
open import Data.Dec
open import Data.Nat
open import Data.Sum
```
-->

```agda
module Data.Int.HIT where
```

# The integers as a HIT

One of the possible characterisations of the [[integers]] is as the
group freely generated by the _monoid_ of natural numbers under
addition. This module constructs this as a higher inductive type:

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

::: warning
While this higher-inductive type is a perfectly workable definition of
the integers _from a mathematical point of view_, the ergonomics of
higher inductive types are still an area of active research. Therefore,
we prefer a "boring" [[inductive representation of the
integers|integers]].
:::

This is an alternative representation of the construction of the group
integers as consisting of pairs $(x , y)\colon \bb{N}^2$, where $(a,b)$
is set identical to $(c, d)$ when $a + d = b + c$. The single generating
path $(a, b) \sim (1 + a, 1 + b)$ can be stretched to obtain this more
familiar quotient, but it has the benefit of provably resulting in a
[[set]] (without [[truncation|set truncation]]). Intuitively, this is
because we only identify points that "used to be distinct".

We can start by proving that all representations of zero are the same:

```agda
zeroes : (n : Nat) → diff 0 0 ≡ 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)$.

```agda
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$.

```agda
offset-negative : (a b : Nat) → diff a (a + b) ≡ diff 0 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 0 b                   ∎

offset-positive : (a b : Nat) → diff (a + b) a ≡ diff b 0
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 0                   ∎
```

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`{.Agda} below packages
everything together with a bow on the top.

```agda
opaque
  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! path ⟩
    diff c ⌜ b + c ⌝ ≡⟨ ap! (+-commutative b c) ⟩
    diff c (c + b)   ≡⟨ offset-negative _ _ ⟩
    diff 0 b         ∎
  same-difference {suc a} {zero} {c} {d} path = sym $
    diff ⌜ c ⌝ d         ≡⟨ ap! (sym path) ⟩
    diff ⌜ suc a + d ⌝ d ≡⟨ ap! (+-commutative (suc a) d) ⟩
    diff (d + suc a) d   ≡⟨ offset-positive _ _ ⟩
    diff (suc a) 0       ∎

  same-difference {suc a} {suc b} {c} {d} path =
    diff (suc a) (suc b) ≡˘⟨ quot _ _ ⟩
    diff a b             ≡⟨ same-difference (suc-inj path) ⟩
    diff c d             ∎
```

<!--
```agda
quot-diamond : (a b : Nat)
             → Square (quot a b) (quot a b)
                      (quot (suc a) (suc b))
                      (quot (suc a) (suc b))
quot-diamond a b i j = hcomp (∂ i ∨ ∂ j) λ where
  k (i = i0) → quot a b j
  k (i = i1) → quot (suc a) (suc b) (j ∧ k)
  k (j = i0) → quot a b i
  k (j = i1) → quot (suc a) (suc b) (i ∧ k)
  k (k = i0) → quot a b (i ∨ j)

quot-triangle : (a b : Nat) (i : I) → diff a b ≡ quot a b i
quot-triangle a b i j = hcomp (∂ j ∨ ~ i) λ where
  k (i = i0) → diff a b
  k (j = i0) → diff a b
  k (k = i0) → diff a b
  k (j = i1) → quot a b (i ∧ k)
```
-->

In the other direction, we must be clever: we use path induction,
defining a type family $\rm{Code}_{a,b}(x)$ such that the fibre of
$\rm{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`{.Agda}. 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.

```agda
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
$\rm{Code}_{a,b}(x)$ by recursion on the integer $x$. Recall that we
want the fibre over $\rm{diff}(c, d)$ to be $a + d = b + c$, so that's
our pick. Now, the `quot`{.Agda} 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.

```agda
  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 $\rm{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`{.Agda} fibration, we must show that $a + b = b + a$, but this is
exactly commutativity of addition on $\bb{N}$.

```agda
  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`{.Agda} and
`Negative`{.Agda}, meaning that we can use positive and negative integer
literals to denote values of `Int`{.Agda}.

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

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

## Canonical representatives

Initially, we note that the type of integers admits a surjection from
the type $\bb{N} \to \bb{N}$, given by sending each pair of naturals to
their `difference`{.Agda}.

```agda
private
  difference-surjection : ∀ x → ∃ (Nat × Nat) (λ (a , b) → (diff a b ≡ x))
  difference-surjection (diff x y) = inc ((x , y) , refl)
  difference-surjection (quot m n i) =
    is-prop→pathp
      (λ i → ∥_∥.squash {A = Σ[ (a , b) ∈ Nat × Nat ] (diff a b ≡ quot m n i)})
      (inc ((m , n) , refl))
      (inc ((suc m , suc n) , refl))
      i
```

What we'll show is that this surjection actually _splits_: Given an
integer, we can find out what natural numbers it came from. Well, not
quite: We can find a reduced representation of that difference. Namely,
suppose we're given the integer $a-b$. We split by cases:

- If $a < b$, then this is the same integer as $0 - (b - a)$;
- If $a > b$, then this is the same integer as $(a - b) - 0$;
- If $a = b$, then this is the same integer as $0 - 0$.

A "canonical form" for an integer is a pair of natural numbers that
represent (under `diff`{.Agda}) the same integer we started with. The
canonicalisation procedure does the split we described above, appealing
to a battery of three lemmas to prove the equality.

```agda
Canonical : Int → Type
Canonical n = Σ[ x ∈ Nat ] Σ[ y ∈ Nat ] (diff x y ≡ n)

canonicalise : (n : Int) → Canonical n
canonicalise = go where
  lemma₁ : ∀ x y → .(x < y) → diff 0 (y - x) ≡ diff x y
  lemma₂ : ∀ x y → .(y < x) → diff (x - y) 0 ≡ diff x y
  lemma₃ : ∀ x y → .(x ≡ y) → diff 0 0       ≡ diff x y

  work : ∀ x y → Canonical (diff x y)
  work x y with ≤-split x y
  ... | inl p       = 0     , y - x , lemma₁ x y p
  ... | inr (inl p) = x - y , 0     , lemma₂ x y p
  ... | inr (inr p) = 0     , 0     , lemma₃ x y p
```

It remains to show that the procedure `work`{.Agda} respects the
quotient. This is a truly gargantuan amount of work, and so it's omitted
from this page. You can unfold it below if you dare:

<details>
<summary>No, really, it's quite ugly.</summary>

```agda
  -- I commend your bravery in unfolding this <details>! These three
  -- lemmas are inductively defined on the natural numbers in a way that
  -- lets us prove that the paths they return respect the Int quotient
  -- without using that Int is a set (because we don't know that yet!)

  lemma₁ zero    (suc y) p = refl
  lemma₁ (suc x) (suc y) p = lemma₁ x y (≤-peel p) ∙ Int.quot x y

  lemma₂ (suc x) zero    p = refl
  lemma₂ (suc x) (suc y) p = lemma₂ x y (≤-peel p) ∙ Int.quot x y

  lemma₃ zero zero p       = refl
  lemma₃ zero (suc y) p    = absurd (zero≠suc p)
  lemma₃ (suc x) zero p    = absurd (suc≠zero p)
  lemma₃ (suc x) (suc y) p = lemma₃ x y (suc-inj p) ∙ Int.quot x y

  abstract
    work-respects-quot
      : ∀ x y → PathP (λ i → Canonical (Int.quot x y i))
        (work x y) (work (suc x) (suc y))
    -- We split on (x, y) but also (1+x,1+y). This is obviously
    -- redundant to a human, but to Agda, we must do this: there is no
    -- link between these two splits.

    work-respects-quot x y with ≤-split x y | ≤-split (suc x) (suc y)
    ... | inl x<y | inl (s≤s x<y') = Σ-pathp refl $ Σ-pathp refl $
      commutes→square (∙-idl _)
    ... | inr (inl x>y) | inr (inl (s≤s x>y')) = Σ-pathp refl $ Σ-pathp refl $
      commutes→square (∙-idl _)
    ... | inr (inr x≡y) | inr (inr x≡y') = Σ-pathp refl $ Σ-pathp refl $
      commutes→square (∙-idl _)

    -- This *barrage* of cases is to handle the cases where e.g. (x < y)
    -- but (1 + x > 1 + y), which is "obviously" impossible. But Agda
    -- doesn't care about what humans think is obvious.
    ... | inl x<y | inr (inl (s≤s x>y))       = absurd (<-asym x<y x>y)
    ... | inl x<y | inr (inr x≡y)             = absurd (<-not-equal x<y (suc-inj x≡y))
    ... | inr (inl x>y) | inl (s≤s x<y)       = absurd (<-asym x>y x<y)
    ... | inr (inr x≡y) | inl (s≤s x<y)       = absurd (<-not-equal x<y x≡y)
    ... | inr (inl x>y) | inr (inr x≡y)       = absurd (<-not-equal x>y (sym (suc-inj x≡y)))
    ... | inr (inr x≡y) | inr (inl (s≤s x>y)) = absurd (<-irrefl (sym x≡y) x>y)

  go : ∀ n → Canonical n
  go (diff x y) = work x y
  go (Int.quot x y i) = work-respects-quot x y i
```

</details>

This _immediately_ implies that the type of integers is a set, because
it's a retract of a set --- namely $\bb{N} \times \bb{N}$!

```agda
instance abstract
  H-Level-Int : ∀ {n} → H-Level Int (2 + n)
  H-Level-Int = basic-instance 2 (retract→is-hlevel 2 into from linv (hlevel 2)) where
    into : (Nat × Nat) → Int
    into (x , y) = diff x y

    from : Int → Nat × Nat
    from x with canonicalise x
    ... | a , b , p = a , b

    linv : ∀ x → into (from x) ≡ x
    linv x with canonicalise x
    ... | a , b , p = p
```

# 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:

```agda
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:

```agda
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(\rm{S}a,\rm{S}b,\rm{S}x,\rm{S}y)$ (`pl` after `pr` and
`pr` after `pl`, respectively) and these _must_ be homotopic:

```agda
         → (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$[^1]:

[^1]: In the diagram, we write $\rm{S}x$ for `suc x`.

~~~{.quiver}
\[\begin{tikzcd}
  {f(a,b,x,y)} && {f(a,b,\rm{S}x,\rm{S}y)} \\
  \\
  {f(\rm{S}a,\rm{S}b, x, y)} && {f(\rm{S}a,\rm{S}b,\rm{S}x,\rm{S}y)}
  \arrow["{pl(a,b,x,y)}", from=1-1, to=3-1]
  \arrow["{pr(a,b,x,y)}", from=1-1, to=1-3]
  \arrow["{pl(a,b,\rm{S}x,\rm{S}y)}"', from=1-3, to=3-3]
  \arrow["{pr(\rm{S}a,\rm{S}b,x,y)}"', from=3-1, to=3-3]
\end{tikzcd}\]
~~~

```agda
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
```

<!--
```agda
_ = is-set
```
-->

However, when the type $X$ we are mapping into `is a set`{.Agda
ident=is-set}, as is the case for the integers themselves, the square is
automatically satisfied, so we can give a simplified recursion
principle:

```agda
Int-rec₂-set :
  ∀ {ℓ} {B : Type ℓ} ⦃ iss-b : H-Level B 2 ⦄
  → (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 abstract
  square
    : (a b x y : Nat)
    → PathP (λ i → pl a b x y i ≡ pl a b (suc x) (suc y) i)
            (pr a b x y) (pr (suc a) (suc b) x y)
  square a b x y = is-set→squarep (λ i j → hlevel 2) _ _ _ _
```

Furthermore, when proving _`propositions`{.Agda ident=is-prop}_ of the
integers, the quotient is automatically respected, so it suffices to
give the case for `diff`{.Agda}:

```agda
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
```

<details>
<summary>There are also variants for binary and ternary predicates.</summary>
```agda
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 1 (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 1 (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
```
</details>

A third possibility for elimination is granted to us by the
canonicalisation procedure: By canonicalising and looking at the
resulting minuend and subtrahend^[keeping in mind that the image of
`canonicalise`{.Agda} is restricted to pairs of the form $(0,1+x)$,
$(1+x,0)$, or $(0,0)$], we can split on an integer based on its sign:

<!--
```agda
abstract
  canonicalise-not-both-suc
    : ∀ x {k n}
    → canonicalise x .fst ≡ suc k
    → ¬ canonicalise x .snd .fst ≡ suc n
  canonicalise-not-both-suc =
    Int-elim-prop {P = λ x → ∀ {k n}
                           → canonicalise x .fst ≡ suc k
                           → ¬ canonicalise x .snd .fst ≡ suc n
                           }
      (λ p → hlevel 1)
      go
    where
      go : ∀ a b {k n}
         → canonicalise (diff a b) .fst ≡ suc k
         → ¬ canonicalise (diff a b) .snd .fst ≡ suc n
      go a b p q with ≤-split a b
      ... | inl x       = absurd (zero≠suc p)
      ... | inr (inl x) = absurd (zero≠suc q)
      ... | inr (inr x) = absurd (zero≠suc q)
```
-->

```agda
Int-elim-by-sign
  : ∀ {ℓ} (P : Int → Type ℓ)
  → (pos : ∀ x → P (diff x 0))
  → (neg : ∀ x → P (diff 0 x))
  → P (diff 0 0)
  → ∀ x → P x
Int-elim-by-sign P pos neg zer x with inspect (canonicalise x)
... | (zero  , zero  , p) , q = subst P p zer
... | (zero  , suc b , p) , q = subst P p (neg (suc b))
... | (suc a , zero  , p) , q = subst P p (pos (suc a))
... | (suc a , suc b , p) , q =
  absurd (canonicalise-not-both-suc x (ap fst q) (ap (fst ∘ snd) q))
```

<!--
```agda
data By-sign-view : Int → Type where
  posv  : ∀ z → By-sign-view (diff z 0)
  negv  : ∀ z → By-sign-view (diff 0 (suc z))

by-sign : ∀ x → By-sign-view x
by-sign = Int-elim-by-sign (λ z → By-sign-view z) posv
  (λ { zero    → posv 0
     ; (suc x) → negv x
     })
  (posv 0)
```
-->

This procedure is useful, for instance, for computing absolute values:

```agda
abs : Int → Nat
abs x with by-sign x
... | posv z = z
... | negv z = suc z

_ : abs -10 ≡ 10
_ = refl
```

# 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".

```agda
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`{.Agda}, we
have that predecessor and successor are inverses, since applying both
(in either order) takes $(a, b)$ to $(1 + a, 1 + b)$.

```agda
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

```agda
_+ℤ_ : Int → Int → Int
diff a b +ℤ diff c d = diff (a + c) (b + d)
diff x y +ℤ quot m n i =
  (quot (x + m) (y + n) ∙ sym (ap₂ diff (+-sucr x m) (+-sucr y n))) i
quot m n i +ℤ diff x y = quot (m + x) (n + y) i
quot m n i +ℤ quot m' n' j =
  is-set→squarep (λ i j → hlevel 2)
    (λ j → quot (m + m') (n + n') j)
    (quot (m + m') (n + n') ∙ sym (ap₂ diff (+-sucr m m') (+-sucr n n')))
    ( quot (suc (m + m')) (suc (n + n'))
    ∙ sym (ap₂ diff (ap suc (+-sucr m m')) (ap suc (+-sucr n n'))))
    (λ j → quot (m + suc m') (n + suc n') j)
    i j
```

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

```agda
+ℤ-associative : (x y z : Int) → x +ℤ (y +ℤ z) ≡ (x +ℤ y) +ℤ z
+ℤ-zerol       : (x : Int)     → 0 +ℤ x ≡ x
+ℤ-zeror       : (x : Int)     → x +ℤ 0 ≡ x
+ℤ-commutative : (x y : Int)   → x +ℤ y ≡ y +ℤ x
```

<details>
<summary>See the proofs here</summary>

```agda
abstract
  +ℤ-associative =
    Int-elim₃-prop
      (λ x y z → hlevel 1)
      (λ a b c d e f → ap₂ diff (+-associative a c e) (+-associative b d f))
  +ℤ-zerol = Int-elim-prop (λ x → hlevel 1) (λ a b → refl)
  +ℤ-zeror =
    Int-elim-prop (λ x → hlevel 1) (λ a b → ap₂ diff (+-zeror a) (+-zeror b))
  +ℤ-commutative =
    Int-elim₂-prop (λ x y → hlevel 1)
      (λ a b c d → ap₂ diff (+-commutative a c) (+-commutative b d))
```

</details>

## 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`{.Agda} is very simple, it can be written conveniently without
using `Int-rec`{.Agda}:

```agda
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`{.Agda ident=zeroes}.

```agda
abstract
  +ℤ-inverser : (x : Int) → x +ℤ negate x ≡ 0
  +ℤ-inverser =
    Int-elim-prop (λ _ → hlevel 1) λ where
      a b → diff (a + b) ⌜ b + a ⌝ ≡⟨ ap! (+-commutative b a) ⟩
            diff (a + b) (a + b)   ≡⟨ sym (zeroes (a + b)) ⟩
            diff 0 0               ∎

  +ℤ-inversel : (x : Int) → negate x +ℤ x ≡ 0
  +ℤ-inversel =
    Int-elim-prop (λ _ → hlevel 1) λ where
      a b → diff ⌜ b + a ⌝ (a + b) ≡⟨ ap! (+-commutative b a) ⟩
            diff (a + b) (a + b)   ≡⟨ sym (zeroes (a + b)) ⟩
            diff 0 0               ∎
```

Since `negate`{.Agda} is precisely what's missing for `Nat`{.Agda} 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`{.Agda}:

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

## Multiplication

We now prove that the integers are a _ring_, i.e. that there is a
multiplication operation $x*y$ with 1 as a left/right identity, which is
associative, and additionally distributes over addition on both the left
and the right. It's also commutative --- so $\bb{Z}$ is a _commutative_
ring.

The definition of multiplication is slightly tricky: We use the binomial
theorem. Pretend that $xy$ is really $(a-b)(c-d)$, and expand that to
$(ac+bd) - (ad+bc)$: that's our product. It remains to show that this
respects the defining equation `quot`{.Agda}, which involves some nasty
equations (you can see them in the types of `l₁`{.Agda} and `l₂`{.Agda}
below) --- but this can be done with [the semiring solver].

[the semiring solver]: Data.Nat.Solver.html


<!--
```agda
module _ where
  private abstract
    l₁
      : ∀ a b x y
      → a * x + b * y + (suc a * y + suc b * x)
      ≡ a * y + b * x + (suc a * x + suc b * y)
    l₁ a b x y = nat!

    l₂
      : ∀ a b x y
      → a * x + b * y + (a * suc y + b * suc x)
      ≡ a * y + b * x + (a * suc x + b * suc y)
    l₂ a b x y = nat!

    rhs₁ : ∀ x y m n → diff (x * m + y * n) (x * n + y * m)
                    ≡ diff (x * suc m + y * suc n) (x * suc n + y * suc m)
    rhs₁ x y m n = same-difference (l₂ x y m n)

    rhs₂ : ∀ x y m n
        → diff (m * x + n * y) (m * y + n * x)
        ≡ diff (x + m * x + (y + n * y)) (y + m * y + (x + n * x))
    rhs₂ x y m n = same-difference (l₁ m n x y)
```
-->

```agda
  _*ℤ_ : Int → Int → Int
  diff a b *ℤ diff c d = diff (a * c + b * d) (a * d + b * c)
  diff x y *ℤ quot m n i = rhs₁ x y m n i
  quot m n i *ℤ diff x y = rhs₂ x y m n i
  quot m n i *ℤ quot x y j = is-set→squarep (λ i j → hlevel 2)
    (rhs₂ x y m n) (rhs₁ m n x y)
    (rhs₁ (suc m) (suc n) x y) (rhs₂ (suc x) (suc y) m n) i j
```

We omit the proofs of the arithmetic identities below since they are
essentially induction + calling the semiring solver.

```agda
abstract
  *ℤ-associative : ∀ x y z → x *ℤ (y *ℤ z) ≡ (x *ℤ y) *ℤ z
  *ℤ-commutative : ∀ x y → x *ℤ y ≡ y *ℤ x
  *ℤ-idl : ∀ x → 1 *ℤ x ≡ x
  *ℤ-idr : ∀ x → x *ℤ 1 ≡ x
  *ℤ-distrib-+ℤ-l : ∀ x y z → x *ℤ (y +ℤ z) ≡ (x *ℤ y) +ℤ (x *ℤ z)
  *ℤ-distrib-+ℤ-r : ∀ x y z → (y +ℤ z) *ℤ x ≡ (y *ℤ x) +ℤ (z *ℤ x)
```

<!--
```agda
  *ℤ-associative =
    Int-elim₃-prop (λ _ _ _ → hlevel 1)
      λ a b c d e f → sym (same-difference (lemma a b c d e f))
    where abstract
      lemma
        : ∀ a b c d e f
        → (a * c + b * d) * e + (a * d + b * c) * f + (a * (c * f + d * e) + b * (c * e + d * f))
        ≡ (a * c + b * d) * f + (a * d + b * c) * e + (a * (c * e + d * f) + b * (c * f + d * e))
      lemma a b c d e f = nat!

  *ℤ-commutative =
    Int-elim₂-prop (λ _ _ → hlevel 1) λ a b x y → same-difference (lemma a b x y)
    where abstract
      lemma : ∀ a b x y → a * x + b * y + (x * b + y * a) ≡ a * y + b * x + (x * a + y * b)
      lemma a b x y = nat!

  *ℤ-idl = Int-elim-prop (λ _ → hlevel 1) (λ a b → same-difference (lemma a b))
    where abstract
      lemma : ∀ a b → (a + 0 + 0 + b) ≡ (b + 0 + 0 + a)
      lemma a b = nat!

  *ℤ-idr = Int-elim-prop (λ _ → hlevel 1) (λ a b → same-difference (lemma a b))
    where abstract
      lemma : ∀ a b → a * 1 + b * 0 + b ≡ a * 0 + b * 1 + a
      lemma a b = nat!

  *ℤ-distrib-+ℤ-l = Int-elim₃-prop (λ _ _ _ → hlevel 1)
    λ a b c d e f → same-difference (lemma a b c d e f)
    where abstract
      lemma : ∀ a b c d e f → a * (c + e) + b * (d + f) + (a * d + b * c + (a * f + b * e)) ≡ a * (d + f) + b * (c + e) + (a * c + b * d + (a * e + b * f))
      lemma a b c d e f = nat!

  *ℤ-distrib-+ℤ-r = Int-elim₃-prop (λ _ _ _ → hlevel 1)
    λ a b c d e f → same-difference (lemma a b c d e f)
    where
      lemma : ∀ a b c d e f → (c + e) * a + (d + f) * b + (c * b + d * a + (e * b + f * a)) ≡ (c + e) * b + (d + f) * a + (c * a + d * b + (e * a + f * b))
      lemma a b c d e f = nat!

canonicalise-injective
  : ∀ x y
  → canonicalise x .fst      ≡ canonicalise y .fst
  → canonicalise x .snd .fst ≡ canonicalise y .snd .fst
  → x ≡ y
canonicalise-injective = Int-elim₂-prop (λ _ _ → hlevel 1) λ a b x y p q →
     sym (canonicalise (diff a b) .snd .snd)
  ·· ap₂ diff p q
  ·· canonicalise (diff x y) .snd .snd

instance
  Discrete-Int : Discrete Int
  Discrete-Int = go _ _ where
    go₀ : (a b x y : Nat) → Dec (diff a b ≡ diff x y)
    go₀ a b x y with a + y ≡? b + x
    ... | yes p  = yes (same-difference p)
    ... | no ¬p = no λ ab → ¬p (ℤ-Path.encode a b (diff x y) ab)

    go₁ : (a b : Nat) (y : Int) → Dec (diff a b ≡ y)
    go₁ a b (diff x y) = go₀ a b x y
    go₁ a b (quot m n i) = is-prop→pathp
      (λ i → Dec-is-hlevel 1 (hlevel {T = diff a b ≡ quot m n i} 1))
      (go₀ a b m n)
      (go₀ a b (suc m) (suc n)) i

    go : ∀ x y → Dec (x ≡ y)
    go (diff a b) y = go₁ a b y
    go (quot m n i) y = is-prop→pathp
      (λ i → Dec-is-hlevel 1 (hlevel {T = quot m n i ≡ y} 1))
      (go₁ m n y)
      (go₁ (suc m) (suc n) y) i
```
-->
