W-Types

WTypes.agda

{-# OPTIONS --type-in-type #-}
module WTypes where

data Nada : Set where

data Unit : Set where
  unit : Unit

data Pos₂ : Set where
    P₁ P₂ : Pos₂

record Poly : Set where
  constructor _▹_
  field
    pos : Set
    dir : pos -> Set
open Poly

⦅_⦆ : Poly → Set → Set
⦅ P ▹ D ⦆ X = Σ[ p ∈ P ] (D p → X)

-- well founded trees
data 𝓦 (P : Poly) : Set where
    ⟨_⟩ : ⦅ P ⦆ (𝓦 P) → 𝓦 P
    
-- Example
NatP : Poly
NatP = Pos₂ ▹ λ{  P₁ → Nada 
                ; P₂ → Unit }

Nat : Set 
Nat = 𝓦 NatP

zero : Nat
zero = ⟨ P₁ , (λ ()) ⟩

Suc : Nat → Nat
Suc n = ⟨ (P₂ , λ{ unit → n}) ⟩

Three : Nat 
Three = Suc (Suc (Suc zero))