Documentation

Mathlib.Data.PFunctor.Univariate.Basic

Polynomial functors #

This file defines polynomial functors and the W-type construction as a polynomial functor. (For the M-type construction, see pfunctor/M.lean.)

structure PFunctor :
Type (u + 1)
  • A : Type u

    The head type

  • B : s.AType u

    The child family of types

A polynomial functor P is given by a type A and a family B of types over A. P maps any type α to a new type P.obj α, which is defined as the sigma type Σ x, P.B x → α.

An element of P.obj α is a pair ⟨a, f⟩, where a is an element of a type A and f : B a → α. Think of a as the shape of the object and f as an index to the relevant elements of α.

Instances For
    def PFunctor.Obj (P : PFunctor) (α : Type u_1) :
    Type (max u_2 u_1 u_2)

    Applying P to an object of Type

    Instances For
      def PFunctor.map (P : PFunctor) {α : Type u_1} {β : Type u_2} (f : αβ) :

      Applying P to a morphism of Type

      Instances For
        theorem PFunctor.map_eq (P : PFunctor) {α : Type u_1} {β : Type u_1} (f : αβ) (a : P.A) (g : PFunctor.B P aα) :
        f <$> { fst := a, snd := g } = { fst := a, snd := f g }
        theorem PFunctor.id_map (P : PFunctor) {α : Type u_1} (x : PFunctor.Obj P α) :
        id <$> x = id x
        theorem PFunctor.comp_map (P : PFunctor) {α : Type u_1} {β : Type u_1} {γ : Type u_1} (f : αβ) (g : βγ) (x : PFunctor.Obj P α) :
        (g f) <$> x = g <$> f <$> x
        def PFunctor.W (P : PFunctor) :
        Type u_1

        re-export existing definition of W-types and adapt it to a packaged definition of polynomial functor

        Instances For
          def PFunctor.W.head {P : PFunctor} :
          PFunctor.W PP.A

          root element of a W tree

          Instances For

            children of the root of a W tree

            Instances For

              destructor for W-types

              Instances For

                constructor for W-types

                Instances For

                  Idx identifies a location inside the application of a pfunctor. For F : PFunctor, x : F.obj α and i : F.Idx, i can designate one part of x or is invalid, if i.1 ≠ x.1

                  Instances For
                    def PFunctor.Obj.iget {P : PFunctor} [DecidableEq P.A] {α : Type u_2} [Inhabited α] (x : PFunctor.Obj P α) (i : PFunctor.IdxCat P) :
                    α

                    x.iget i takes the component of x designated by i if any is or returns a default value

                    Instances For
                      @[simp]
                      theorem PFunctor.fst_map {P : PFunctor} {α : Type u} {β : Type u} (x : PFunctor.Obj P α) (f : αβ) :
                      (f <$> x).fst = x.fst
                      @[simp]
                      theorem PFunctor.iget_map {P : PFunctor} [DecidableEq P.A] {α : Type u} {β : Type u} [Inhabited α] [Inhabited β] (x : PFunctor.Obj P α) (f : αβ) (i : PFunctor.IdxCat P) (h : i.fst = x.fst) :
                      def PFunctor.comp (P₂ : PFunctor) (P₁ : PFunctor) :

                      functor composition for polynomial functors

                      Instances For
                        def PFunctor.comp.mk (P₂ : PFunctor) (P₁ : PFunctor) {α : Type} (x : PFunctor.Obj P₂ (PFunctor.Obj P₁ α)) :

                        constructor for composition

                        Instances For
                          def PFunctor.comp.get (P₂ : PFunctor) (P₁ : PFunctor) {α : Type} (x : PFunctor.Obj (PFunctor.comp P₂ P₁) α) :
                          PFunctor.Obj P₂ (PFunctor.Obj P₁ α)

                          destructor for composition

                          Instances For
                            theorem PFunctor.liftp_iff {P : PFunctor} {α : Type u} (p : αProp) (x : PFunctor.Obj P α) :
                            Functor.Liftp p x a f, x = { fst := a, snd := f } ((i : PFunctor.B P a) → p (f i))
                            theorem PFunctor.liftp_iff' {P : PFunctor} {α : Type u} (p : αProp) (a : P.A) (f : PFunctor.B P aα) :
                            Functor.Liftp p { fst := a, snd := f } (i : PFunctor.B P a) → p (f i)
                            theorem PFunctor.liftr_iff {P : PFunctor} {α : Type u} (r : ααProp) (x : PFunctor.Obj P α) (y : PFunctor.Obj P α) :
                            Functor.Liftr r x y a f₀ f₁, x = { fst := a, snd := f₀ } y = { fst := a, snd := f₁ } ((i : PFunctor.B P a) → r (f₀ i) (f₁ i))
                            theorem PFunctor.supp_eq {P : PFunctor} {α : Type u} (a : P.A) (f : PFunctor.B P aα) :
                            Functor.supp { fst := a, snd := f } = f '' Set.univ