W-types in agda

wtype.agda

-- Based on https://mazzo.li/epilogue/index.html%3Fp=324.html

data W (S : Set) (P : S → Set) : Set where
  _◁_ : (s : S) → (P s → W S P) → W S P

data 𝟘 : Set where

data 𝟙 : Set where
  ● : 𝟙

data 𝟚 : Set where
  ▼ : 𝟚
  ▲ : 𝟚

Ψ : {A : Set} → 𝟘 → A
Ψ ()

-- Natural numbers
ℕ : Set
ℕ = W 𝟚 λ { ▼ → 𝟘; ▲ → 𝟙 }

zero : ℕ
suc  : ℕ → ℕ

zero  = ▼ ◁ Ψ
suc n = ▲ ◁ λ { ● → n }

-- Finite types
Fin : ℕ → Set
Fin n = W 𝟚 λ { ▼ → 𝟘; ▲ → 𝟙 }

fzero : ∀{n} → Fin (suc n)
fzero = ▼ ◁ Ψ

fsuc : ∀{n} → Fin n → Fin (suc n)
fsuc x = ▲ ◁ λ { ● → x }

-- Unlabelled binary trees
Tree : Set
Tree = W 𝟚 λ { ▼ → 𝟘; ▲ → 𝟚 }

leaf : Tree
node : Tree → Tree → Tree

leaf     = ▼ ◁ Ψ
node l r = ▲ ◁ λ { ▼ → l; ▲ → r }


-- Sigma types
data Σ (S : Set) (P : S → Set) : Set where
  _,_ : (s : S) → P s → Σ S P