Documentation

Mathlib.Data.W.Constructions

Examples of W-types #

We take the view of W types as inductive types. Given α : Type and β : α → Type→ 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α :

zero: WType.Natα
succ: WType.Natα

The constructors for the naturals

Instances For

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.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 ⊕ PUnit) :

↑(Equiv.symm WType.NatαEquivPUnitSumPUnit) b = match b with | Sum.inl val => WType.Natα.zero | Sum.inr val => WType.Natα.succ

def WType.NatαEquivPUnitSumPUnit :

WType.Natα ≃ PUnit ⊕ PUnit

WType.Natα is equivalent to PUnit ⊕ 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) :

nil: {γ : Type u} → WType.Listα γ
cons: {γ : Type u} → γ → WType.Listα γ

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
→ List γ
| cons x₁ : List γ → List γ
|   ⋮      γ many times
→ List γ
|   ⋮      γ many times
⋮      γ many times

Instances For

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 | WType.Listα.cons a => PUnit

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

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

def WType.ListαEquivPUnitSum (γ : Type u) :

WType.Listα γ ≃ PUnit ⊕ γ

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.