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 #

inductive WType.Natα :

The constructors for the naturals

Instances For

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

    Equations

    The isomorphism from the naturals to its corresponding WType

    Equations

    The isomorphism from the WType of the naturals to the naturals

    Equations

    The naturals are equivalent to their associated WType

    Equations

    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) :

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

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

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

      The isomorphism from lists to the WType construction of lists

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

      The isomorphism from the WType construction of lists to lists

      Equations

      Lists are equivalent to their associated WType

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

      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.