Skip to content

Instantly share code, notes, and snippets.

@louisswarren louisswarren/wtype.agda
Last active Jan 29, 2020

Embed
What would you like to do?
W-types in 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 }
-- 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.