PLFA: Relations

Programming Language Foundations in Agda, Relations: Inductive definition of relations.

Dependent types are introduced in a very confusing way. Here is some explanation. The definition of ≤ is given by

1data _≤_ : ℕ → ℕ → Set where
2  z≤n : ∀ {n : ℕ} → zero ≤ n
3  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n
4s

Note the implicit argument marked by the apperance of curly brackets {}. Here zero ≤ n, m ≤ n, suc m ≤ suc n are all dependent types, or family of types (remember Curry-Howard). z≤n and s≤s are type constructors. For fixed n:ℕ, zero ≤ n is a type.

The proof of _ : 2 ≤ 4, given by

1_ : 2 ≤ 4
2_ = s≤s (s≤s z≤n)

is really

1_ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2}))

where

• the type z≤n {2} is zero ≤ 2,
• the type s≤s {0} {2} is suc 0 ≤ suc 2,
• the type s≤s {1} {3} is suc 2 ≤ suc 4.