# mathlibdocumentation

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, W_type β, 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 #

• W_type.equiv_nat: the construction of the naturals as a W-type is equivalent to nat
• W_type.equiv_list: the construction of lists on a type γ as a W-type is equivalent to list γ
inductive W_type.nat_α  :
Type

The constructors for the naturals

Instances for W_type.nat_α
@[protected, instance]
Equations
def W_type.nat_β  :
W_type.nat_α → Type

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

Equations
Instances for W_type.nat_β
@[protected, instance]
Equations
@[simp]
def W_type.of_nat  :

The isomorphism from the naturals to its corresponding W_type

Equations
@[simp]
def W_type.to_nat  :

The isomorphism from the W_type of the naturals to the naturals

Equations

The naturals are equivalent to their associated W_type

Equations

W_type.nat_α is equivalent to punit ⊕ punit. This is useful when considering the associated polynomial endofunctor.

Equations
@[simp]
theorem W_type.nat_α_equiv_punit_sum_punit_apply (c : W_type.nat_α) :
= W_type.nat_α_equiv_punit_sum_punit._match_1 c
@[simp]
theorem W_type.nat_α_equiv_punit_sum_punit_symm_apply (b : punit punit) :
= W_type.nat_α_equiv_punit_sum_punit._match_2 b
inductive W_type.list_α (γ : Type u) :
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 W_type.list_α
@[protected, instance]
def W_type.list_α.inhabited (γ : Type u) :
Equations
def W_type.list_β (γ : Type u) :
Type u

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

Equations
Instances for W_type.list_β
@[protected, instance]
def W_type.list_β.inhabited (γ : Type u) (hd : γ) :
Equations
@[simp]
def W_type.of_list (γ : Type u) :
list γ

The isomorphism from lists to the W_type construction of lists

Equations
@[simp]
def W_type.to_list (γ : Type u) :
list γ

The isomorphism from the W_type construction of lists to lists

Equations
theorem W_type.left_inv_list (γ : Type u) :
theorem W_type.right_inv_list (γ : Type u) :
def W_type.equiv_list (γ : Type u) :
list γ

Lists are equivalent to their associated W_type

Equations
def W_type.list_α_equiv_punit_sum (γ : Type u) :

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

Equations