DefinitionalEquality.agda

module DefinitionalEquality where

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

subst : {A : Set}(P : A -> Set){x y : A} -> x == y -> P y -> P x
subst {A} P refl p = p

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

-- This formulation of the associativity law guarantees that for closed n, but
-- possibly open m and p the law holds definitionally.

assoc : (n : Nat) -> (\m p -> n + (m + p)) == (\m p -> (n + m) + p)
assoc zero    = refl
assoc (suc n) = subst (\ ∙ -> f ∙ == f (\m p -> ((n + m) + p)))
                      (assoc n) refl
  where
    f = \(g : Nat -> Nat -> Nat)(m p : Nat) -> suc (g m p)