Single case induction

SingleCaseInduction.agda

module SingleCaseInduction where

-- Usual definition of ℕ
data N : Set where
  z : N
  s : N → N


-- Single case definition of ℕ
data _+_ (A : Set) (B : Set) : Set where
  inl : A → A + B
  inr : B → A + B

record ⊤ : Set where

data ℕ : Set where
  s : (⊤ + ℕ) → ℕ

-- Usage…
z₁ : N
z₁ = z
1₁ : N
1₁ = s z
2₁ : N
2₁ = s (s z)

z₂ : ℕ
z₂ = s (inl _)
1₂ : ℕ
1₂ = s (inr (s (inl _)))
2₂ : ℕ
2₂ = s (inr (s (inr (s (inl _)))))