# 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 to Nat
• WType.equivList: the construction of lists on a type γ as a W-type is equivalent to List γ
inductive WType.Natα :

The constructors for the naturals

Instances For

The arity of the constructors for the naturals, zero takes no arguments, succ takes one

Equations
Instances For
Equations

The isomorphism from the naturals to its corresponding WType

Equations
Instances For

The isomorphism from the WType of the naturals to the naturals

Equations
• .toNat = 0
• .toNat = (f ()).toNat.succ
Instances For

The naturals are equivalent to their associated WType

Equations
Instances For
@[simp]
theorem WType.NatαEquivPUnitSumPUnit_apply (c : WType.Natα) :
WType.NatαEquivPUnitSumPUnit c = match c with | WType.Natα.zero => | WType.Natα.succ =>

WType.Natα is equivalent to PUnit ⊕ PUnit. This is useful when considering the associated polynomial endofunctor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
inductive WType.Listα (γ : Type u) :

The constructors for lists. There is "one constructor cons x for each x : γ", since we view List γ as

| nil : List γ
| cons x₀ : List γ → List γ
| cons x₁ : List γ → List γ
|   ⋮      γ many times

• nil: {γ : Type u} →
• cons: {γ : Type u} → γ
Instances For
instance WType.instInhabitedListα (γ : Type u) :
Equations
• = { default := WType.Listα.nil }
def WType.Listβ (γ : Type u) :
Type u

The arities of each constructor for lists, nil takes no arguments, cons hd takes one

Equations
Instances For
instance WType.instInhabitedListβCons (γ : Type u) (hd : γ) :
Equations
def WType.ofList (γ : Type u) :
List γWType ()

The isomorphism from lists to the WType construction of lists

Equations
Instances For
def WType.toList (γ : Type u) :
WType ()List γ

The isomorphism from the WType construction of lists to lists

Equations
Instances For
def WType.equivList (γ : Type u) :
WType () List γ

Lists are equivalent to their associated WType

Equations
• = { toFun := , invFun := , left_inv := , right_inv := }
Instances For

WType.Listα is equivalent to γ with an extra point. This is useful when considering the associated polynomial endofunctor

Equations
• One or more equations did not get rendered due to their size.
Instances For