# Documentation

Mathlib.Data.W.Constructions

# Examples of W-types #

We take the view of W types as inductive types. Given α : Type and β : α → Type→ 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

The isomorphism from the naturals to its corresponding WType

Equations

The isomorphism from the WType of the naturals to the naturals

Equations

The naturals are equivalent to their associated WType

Equations
@[simp]
theorem WType.NatαEquivPUnitSumPUnit_symm_apply (b : ) :
= match b with | Sum.inl val => WType.Natα.zero | Sum.inr val => WType.Natα.succ

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

Equations
• One or more equations did not get rendered due to their size.
inductive WType.Listα (γ : Type u) :
• nil: {γ : Type u} →
• cons: {γ : 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
→ List γ
| cons x₁ : List γ → List γ
|   ⋮      γ many times
→ List γ
|   ⋮      γ many times
⋮      γ many times

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
• = match x with | WType.Listα.nil => PEmpty | => PUnit
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
def WType.toList (γ : Type u) :
WType ()List γ

The isomorphism from the WType construction of lists to lists

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

Lists are equivalent to their associated WType

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

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.