open import 1Lab.Type.Dec
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.Nat

module Data.Int.Inductive where

Inductive Integers🔗

The inductive integers (or built-in integers) are the type generated by the two constructors pos and negsuc, as below, but without the primes:

module _ where private
  data Int' : Type where
    pos'    : Nat → Int'
    negsuc' : Nat → Int'

This type is important to have around because it is the type of integers that Agda privileges as a built-in:

open import Agda.Builtin.Int public

As the names indicate, these constructors are meant to represent a positive integer, and the negation of a successor of a natural number, i.e. negsuc is the map taking $n$ to $-(n + 1)$.

_ℕ-_ : Nat → Nat → Int
x     ℕ- zero  = pos x
zero  ℕ- suc y = negsuc y
suc x ℕ- suc y = x ℕ- y

We can decide equality of two Int's by comparing their underlying naturals when the constructors match (i.e. pos/pos or negsuc/negsuc):

Discrete-Int : Discrete Int
Discrete-Int (pos x) (pos y) with Discrete-Nat x y
... | yes p = yes (ap pos p)
... | no ¬p = no λ path → ¬p (ap (λ { (pos x) → x ; (negsuc _) → zero }) path)

Discrete-Int (negsuc x) (negsuc y) with Discrete-Nat x y
... | yes p = yes (ap negsuc p)
... | no ¬p = no λ path → ¬p (ap (λ { (negsuc x) → x ; (pos _) → zero }) path)

And in case the constructors are mismatched, there can be no path between them:

Discrete-Int (pos x) (negsuc y) =
  no λ path → subst (λ { (pos x) → ⊤ ; (negsuc _) → ⊥ }) path tt
Discrete-Int (negsuc x) (pos y) =
  no λ path → subst (λ { (pos x) → ⊥ ; (negsuc _) → ⊤ }) path tt

The integers are characterised as being the free type with an equivalence. This equivalence is the successor function:

suc-int : Int → Int
suc-int (pos n)          = pos (suc n)
suc-int (negsuc zero)    = pos zero
suc-int (negsuc (suc n)) = negsuc n

pred-int : Int → Int
pred-int (pos zero)    = negsuc zero
pred-int (pos (suc n)) = pos n
pred-int (negsuc n)    = negsuc (suc n)

suc-pred : (x : Int) → suc-int (pred-int x) ≡ x
suc-pred (pos zero) = refl
suc-pred (pos (suc x)) = refl
suc-pred (negsuc x) = refl

pred-suc : (x : Int) → pred-int (suc-int x) ≡ x
pred-suc (pos x) = refl
pred-suc (negsuc zero) = refl
pred-suc (negsuc (suc x)) = refl

suc-equiv : Int ≃ Int
suc-equiv = Iso→Equiv (suc-int , iso pred-int suc-pred pred-suc)