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α

instance WType.instInhabitedNatα : Inhabited Natα

Equations

• WType.instInhabitedNatα = { default := WType.Natα.zero }

def WType.Natβ : Natα → Type

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

Equations

• WType.Natβ WType.Natα.zero = Empty
• WType.Natβ WType.Natα.succ = Unit

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

Equations

• WType.instInhabitedNatβSucc = { default := () }

def WType.ofNat : ℕ → WType Natβ

The isomorphism from the naturals to its corresponding WType

Equations

• WType.ofNat Nat.zero = WType.mk WType.Natα.zero Empty.elim
• WType.ofNat n.succ = WType.mk WType.Natα.succ fun (x : WType.Natβ WType.Natα.succ) => WType.ofNat n

def WType.toNat : WType Natβ → ℕ

The isomorphism from the WType of the naturals to the naturals

Equations

• (WType.mk WType.Natα.zero f).toNat = 0
• (WType.mk WType.Natα.succ f).toNat = (f ()).toNat.succ

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

Equations

• WType.equivNat = { toFun := WType.toNat, invFun := WType.ofNat, left_inv := WType.leftInverse_nat, right_inv := WType.rightInverse_nat }

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.

Equations

• One or more equations did not get rendered due to their size.

@[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α γ

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

Equations

• WType.instInhabitedListα γ = { default := WType.Listα.nil }

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

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

Equations

• WType.Listβ γ WType.Listα.nil = PEmpty.{?u.156 + 1}
• WType.Listβ γ (WType.Listα.cons a) = PUnit.{?u.161 + 1}

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

Equations

• WType.instInhabitedListβCons γ hd = { default := PUnit.unit }

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

The isomorphism from lists to the WType construction of lists

Equations

• WType.ofList γ [] = WType.mk WType.Listα.nil PEmpty.elim
• WType.ofList γ (hd :: tl) = WType.mk (WType.Listα.cons hd) fun (x : WType.Listβ γ (WType.Listα.cons hd)) => WType.ofList γ tl

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

The isomorphism from the WType construction of lists to lists

Equations

• WType.toList γ (WType.mk WType.Listα.nil f) = []
• WType.toList γ (WType.mk (WType.Listα.cons hd) f) = hd :: WType.toList γ (f PUnit.unit)

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

Equations

• WType.equivList γ = { toFun := WType.toList γ, invFun := WType.ofList γ, left_inv := ⋯, right_inv := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.