data Bool : Set where true : Bool false : Bool data ℕ : Set where zero : ℕ succ : ℕ -> ℕ _+_ : ℕ -> ℕ -> ℕ zero + m = m succ n + m = succ (n + m)