mathlib3 documentation

data.W.constructions

Examples of W-types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
inductive W_type.nat_α  :
Type

The constructors for the naturals

Instances for W_type.nat_α
source
@[protected, instance]
def W_type.nat_α.inhabited  :
inhabited W_type.nat_α
Equations
source
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_β
source
@[protected, instance]
def W_type.nat_β.inhabited  :
inhabited (W_type.nat_β W_type.nat_α.succ)
Equations
source
@[simp]
def W_type.of_nat  :
ℕ → W_type W_type.nat_β

The isomorphism from the naturals to its corresponding W_type

Equations
source
@[simp]
def W_type.to_nat  :
W_type W_type.nat_β → ℕ

The isomorphism from the W_type of the naturals to the naturals

Equations
source
theorem W_type.left_inv_nat  :
function.left_inverse W_type.of_nat W_type.to_nat
source
theorem W_type.right_inv_nat  :
function.right_inverse W_type.of_nat W_type.to_nat
source
def W_type.equiv_nat  :
W_type W_type.nat_β ≃ ℕ

The naturals are equivalent to their associated W_type

Equations
source
def W_type.nat_α_equiv_punit_sum_punit  :
W_type.nat_α ≃ punit ⊕ punit

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

Equations
source
@[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
source
@[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
source
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_α
source
@[protected, instance]
def W_type.list_α.inhabited (γ : Type u) :
inhabited (W_type.list_α γ)
Equations
source
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_β
source
@[protected, instance]
def W_type.list_β.inhabited (γ : Type u) (hd : γ) :
inhabited (W_type.list_β γ (W_type.list_α.cons hd))
Equations
source
@[simp]
def W_type.of_list (γ : Type u) :
list γ → W_type (W_type.list_β γ)

The isomorphism from lists to the W_type construction of lists

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

The isomorphism from the W_type construction of lists to lists

Equations
source
theorem W_type.left_inv_list (γ : Type u) :
function.left_inverse (W_type.of_list γ) (W_type.to_list γ)
source
theorem W_type.right_inv_list (γ : Type u) :
function.right_inverse (W_type.of_list γ) (W_type.to_list γ)
source
def W_type.equiv_list (γ : Type u) :
W_type (W_type.list_β γ) ≃ list γ

Lists are equivalent to their associated W_type

Equations
source
def W_type.list_α_equiv_punit_sum (γ : Type u) :
W_type.list_α γ ≃ punit ⊕ γ

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

Equations