Functions as Tuple Sets

In a language like Agda, we usually write relationships, as, well, functions. For instance, we might define addition and multiplication on the natural numbers as follows:

open import Agda.Primitive
open import Agda.Builtin.Equality
data ℕ : Set where
    Z : ℕ
    S  : ℕ → ℕ

add : ℕ → ℕ → ℕ
add Z m = m
add (S n) m = S (add n m)

mul : ℕ → ℕ → ℕ
mul Z m = Z
mul (S n) m = add m (mul n m)

However, this is not the only way to define these relationships.

Functions as Types

The other way to describe this is as follows:

data Add : ℕ → ℕ → ℕ → Set where
    Add-Z : ∀ {m} → Add Z m m
    Add-S : ∀ {n m k} → Add n m k → Add (S n) m (S k)

data Mul : ℕ → ℕ → ℕ → Set where
    Mul-Z : ∀ {m} → Mul Z m Z
    Mul-S : ∀ {n m k k'} → Mul n m k → Add m k k' → Mul (S n) m k'

Here, the interpretation of add m n k is $m + n \equiv k$

Add→add : ∀ n m {k} → Add n m k → add n m ≡ k
Add→add Z m Add-Z = refl
Add→add (S n) m (Add-S p) rewrite Add→add n m p = refl

add→Add : ∀ n m {k} → add n m ≡ k → Add n m k
add→Add Z m refl = Add-Z
add→Add (S n) m refl = Add-S (add→Add n m refl)


Mul→mul : ∀ n m {k} → Mul n m k → mul n m ≡ k
Mul→mul Z m Mul-Z = refl
Mul→mul (S n) m (Mul-S p q) rewrite Mul→mul n m p = Add→add m _ q

mul→Mul : ∀ n m {k} → mul n m ≡ k → Mul n m k
mul→Mul Z m refl = Mul-Z
mul→Mul (S n) m refl = Mul-S (mul→Mul n m refl) (add→Add m _ refl)