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: WType.Natα
• succ: WType.Natα

instance WType.instInhabitedNatα : Inhabited WType.Natα

Equations

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

def WType.Natβ : WType.Natα → Type

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

Equations

• WType.Natβ x = match x with | WType.Natα.zero => Empty | WType.Natα.succ => Unit

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

Equations

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

def WType.ofNat : ℕ → WType 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 (Nat.succ n) = WType.mk WType.Natα.succ fun (x : WType.Natβ WType.Natα.succ) => WType.ofNat n

def WType.toNat : WType WType.Natβ → ℕ

The isomorphism from the WType of the naturals to the naturals

Equations

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

theorem WType.leftInverse_nat : Function.LeftInverse WType.ofNat WType.toNat

theorem WType.rightInverse_nat : Function.RightInverse WType.ofNat WType.toNat

def WType.equivNat : WType 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 }

@[simp]

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

@[simp]

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

def WType.NatαEquivPUnitSumPUnit : WType.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.

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} → WType.Listα γ
• cons: {γ : Type u} → γ → WType.Listα γ

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

Equations

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

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

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

Equations

• WType.Listβ γ x = match x with | WType.Listα.nil => PEmpty.{u + 1} | WType.Listα.cons a => PUnit.{u + 1}

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

Equations

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

def WType.ofList (γ : Type u) : List γ → WType (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 (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 (WType.ofList γ) (WType.toList γ)

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

def WType.equivList (γ : Type u) : WType (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) : WType.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.