gistfile1.agda

module WTypes where

import Level

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

data ⊤ : Set where
  ⟨⟩ : ⊤

data ⊥ : Set where

_!_ : ⊥ → (A : Set) → A
() ! t

data Bool : Set where
  tt : Bool
  ff : Bool

If_Then_Else_ : ∀ {α} Bool → Set α → Set α → Set α
If tt Then t Else f = t
If ff Then t Else f = f

ℕ : Set
ℕ = W Bool λ b → If b Then ⊤ Else ⊥

zero : ℕ
zero = ff ◁ λ z → z ! ℕ

succ : ℕ → ℕ
succ n = tt ◁ λ _ → n

rec : {S : Set}           →
      {T : S → Set}       →
      {P : W S T → Set}   →
      (u : W S T)         →
      (p : (s : S)               →
           (f : T s → W S T)     →
           ((t : T s) → P (f t)) →
           P (s ◁ f)
      ) → P u
rec {S}{T}{P} (s ◁ f) p = p s f (λ t → rec {S}{T}{P} (f t) p)

plus : ℕ → ℕ → ℕ
plus x y =
  rec x (λ { tt → λ f h → succ (h ⟨⟩)
           ; ff → λ f h → y
           })