Examples of W-types #
We take the view of W types as inductive types.
Given α : Type
and β : α → Type
, the W type determined by this data, WType β
, is the
inductively with constructors from α
and arities of each constructor a : α
given by β a
.
This file contains Nat
and List
as examples of W types.
Main results #
WType.equivNat
: the construction of the naturals as a W-type is equivalent toNat
WType.equivList
: the construction of lists on a typeγ
as a W-type is equivalent toList γ
The isomorphism from the naturals to its corresponding WType
Equations
- WType.ofNat Nat.zero = WType.mk WType.Natα.zero Empty.elim
- WType.ofNat (Nat.succ n) = WType.mk WType.Natα.succ fun x => WType.ofNat n
Instances For
The isomorphism from the WType
of the naturals to the naturals
Equations
- WType.toNat (WType.mk WType.Natα.zero f) = 0
- WType.toNat (WType.mk WType.Natα.succ f) = Nat.succ (WType.toNat (f ()))
Instances For
The naturals are equivalent to their associated WType
Instances For
WType.Natα
is equivalent to PUnit ⊕ PUnit
.
This is useful when considering the associated polynomial endofunctor.
Instances For
The isomorphism from lists to the WType
construction of lists
Equations
- WType.ofList γ [] = WType.mk WType.Listα.nil PEmpty.elim
- WType.ofList γ (hd :: tl) = WType.mk (WType.Listα.cons hd) fun x => WType.ofList γ tl
Instances For
The isomorphism from the WType
construction of lists to lists
Equations
- WType.toList γ (WType.mk WType.Listα.nil f) = []
- WType.toList γ (WType.mk (WType.Listα.cons hd) f) = hd :: WType.toList γ (f PUnit.unit)
Instances For
Lists are equivalent to their associated WType
Instances For
WType.Listα
is equivalent to γ
with an extra point.
This is useful when considering the associated polynomial endofunctor