mathlib documentation

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 #

inductive W_type.nat_α  :
Type

The constructors for the naturals

Instances for W_type.nat_α
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_β
@[simp]

The isomorphism from the W_type of the naturals to the naturals

Equations

W_type.nat_α is equivalent to punitpunit. 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 c = 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.symm) b = W_type.nat_α_equiv_punit_sum_punit._match_2 b
inductive W_type.list_α (γ : Type u) :
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]
Equations
def W_type.list_β (γ : Type u) :
W_type.list_α γ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) :

The isomorphism from lists to the W_type construction of lists

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

The isomorphism from the W_type construction of lists to lists

Equations
def W_type.equiv_list (γ : Type u) :

Lists are equivalent to their associated W_type

Equations

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

Equations