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α : Type

The constructors for the naturals

• zero : Natα
• succ : Natα

@[implicit_reducible]

instance WType.instInhabitedNatα : Inhabited Natα

def WType.Natβ : Natα → Type

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

@[implicit_reducible]

instance WType.instInhabitedNatβSucc : Inhabited (Natβ Natα.succ)

def WType.ofNat : ℕ → WType Natβ

The isomorphism from the naturals to its corresponding WType

def WType.toNat : WType Natβ → ℕ

The isomorphism from the WType of the naturals to the naturals

theorem WType.leftInverse_nat : Function.LeftInverse ofNat toNat

theorem WType.rightInverse_nat : Function.RightInverse ofNat toNat

def WType.equivNat : WType Natβ ≃ ℕ

The naturals are equivalent to their associated WType

def WType.NatαEquivPUnitSumPUnit : Natα ≃ PUnit.{u + 1} ⊕ PUnit.{u_1 + 1}

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

@[simp]

theorem WType.NatαEquivPUnitSumPUnit_symm_apply (b : PUnit.{u + 1} ⊕ PUnit.{u_1 + 1}) : NatαEquivPUnitSumPUnit.symm b = match b with | Sum.inl val => Natα.zero | Sum.inr val => Natα.succ

@[simp]

theorem WType.NatαEquivPUnitSumPUnit_apply (c : Natα) : NatαEquivPUnitSumPUnit c = match c with | Natα.zero => Sum.inl PUnit.unit | Natα.succ => Sum.inr PUnit.unit

inductive WType.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

• nil {γ : Type u} : Listα γ
• cons {γ : Type u} : γ → Listα γ

@[implicit_reducible]

instance WType.instInhabitedListα (γ : Type u) : Inhabited (Listα γ)

def WType.Listβ (γ : Type u) : Listα γ → Type u

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

@[implicit_reducible]

instance WType.instInhabitedListβCons (γ : Type u) (hd : γ) : Inhabited (Listβ γ (Listα.cons hd))

def WType.ofList (γ : Type u) : List γ → WType (Listβ γ)

The isomorphism from lists to the WType construction of lists

def WType.toList (γ : Type u) : WType (Listβ γ) → List γ

The isomorphism from the WType construction of lists to lists

theorem WType.leftInverse_list (γ : Type u) : Function.LeftInverse (ofList γ) (toList γ)

theorem WType.rightInverse_list (γ : Type u) : Function.RightInverse (ofList γ) (toList γ)

def WType.equivList (γ : Type u) : WType (Listβ γ) ≃ List γ

Lists are equivalent to their associated WType

def WType.ListαEquivPUnitSum (γ : Type u) : Listα γ ≃ PUnit.{v + 1} ⊕ γ

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