w.agda

data W (S : Set) (P : S -> Set) : Set where
  sup : (s : S) (f : P s -> W S P) -> W S P

data ⊥ : Set where

record ⊤ : Set where

data Bool : Set where
  tt : Bool
  ff : Bool
Nat : Set
Nat = W Bool (λ { tt -> ⊤ 
                ; ff -> ⊥ })

zero : Nat
zero = sup ff (λ ())

suc : Nat -> Nat
suc n = sup tt (λ _ -> n)