# Documentation

Mathlib.Data.W.Constructions

# 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

Instances For

The isomorphism from the naturals to its corresponding WType

Equations
Instances For

The isomorphism from the WType of the naturals to the naturals

Equations
Instances For

The naturals are equivalent to their associated WType

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

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

Instances For
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

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

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

Instances For
instance WType.instInhabitedListβCons (γ : Type u) (hd : γ) :
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

Instances For

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

Instances For