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 Mathlib/Data/PFunctor/Univariate/M.lean.)

structure PFunctor :
Type (max (uA + 1) (uB + 1))

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 α, which is defined as the sigma type Σ x, P.B x → α.

An element of P α 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 α.

  • A : Type uA

    The head type

  • B : self.AType uB

    The child family of types

Instances For
    def PFunctor.Obj (P : PFunctor.{uA, uB}) (α : Type v) :
    Type (max v uA uB)

    Applying P to an object of Type

    Equations
    • P α = ((x : P.A) × (P.B xα))
    Instances For
      def PFunctor.map (P : PFunctor.{uA, uB}) {α : Type v₁} {β : Type v₂} (f : αβ) :
      P αP β

      Applying P to a morphism of Type

      Equations
      Instances For
        @[simp]
        theorem PFunctor.map_eq_map (P : PFunctor.{uA, uB}) {α β : Type v} (f : αβ) (x : P α) :
        f <$> x = P.map f x

        We prefer PFunctor.map to Functor.map because it is universe-polymorphic.

        @[simp]
        theorem PFunctor.map_eq (P : PFunctor.{uA, uB}) {α : Type v₁} {β : Type v₂} (f : αβ) (a : P.A) (g : P.B aα) :
        P.map f a, g = a, f g
        @[simp]
        theorem PFunctor.id_map (P : PFunctor.{uA, uB}) {α : Type v₁} (x : P α) :
        P.map id x = x
        @[simp]
        theorem PFunctor.map_map (P : PFunctor.{uA, uB}) {α : Type v₁} {β : Type v₂} {γ : Type v₃} (f : αβ) (g : βγ) (x : P α) :
        P.map g (P.map f x) = P.map (g f) x
        def PFunctor.W (P : PFunctor.{uA, uB}) :
        Type (max uA uB)

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

        Equations
        Instances For

          The root element of a W tree

          Equations
          Instances For
            def PFunctor.W.children {P : PFunctor.{uA, uB}} (x : P.W) :
            P.B x.headP.W

            The children of the root of a W tree

            Equations
            Instances For
              def PFunctor.W.dest {P : PFunctor.{uA, uB}} :
              P.WP P.W

              The destructor for W-types

              Equations
              Instances For
                def PFunctor.W.mk {P : PFunctor.{uA, uB}} :
                P P.WP.W

                The constructor for W-types

                Equations
                Instances For
                  @[simp]
                  theorem PFunctor.W.dest_mk {P : PFunctor.{uA, uB}} (p : P P.W) :
                  (mk p).dest = p
                  @[simp]
                  theorem PFunctor.W.mk_dest {P : PFunctor.{uA, uB}} (p : P.W) :
                  mk p.dest = p
                  def PFunctor.Idx (P : PFunctor.{uA, uB}) :
                  Type (max uA uB)

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

                  Equations
                  Instances For
                    def PFunctor.Obj.iget {P : PFunctor.{uA, uB}} [DecidableEq P.A] {α : Type u_1} [Inhabited α] (x : P α) (i : P.Idx) :
                    α

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

                    Equations
                    Instances For
                      @[simp]
                      theorem PFunctor.fst_map {P : PFunctor.{uA, uB}} {α : Type v₁} {β : Type v₂} (x : P α) (f : αβ) :
                      (P.map f x).fst = x.fst
                      @[simp]
                      theorem PFunctor.iget_map {P : PFunctor.{uA, uB}} {α : Type v₁} {β : Type v₂} [DecidableEq P.A] [Inhabited α] [Inhabited β] (x : P α) (f : αβ) (i : P.Idx) (h : i.fst = x.fst) :
                      (P.map f x).iget i = f (x.iget i)

                      Composition for polynomial functors

                      Equations
                      • P₂.comp P₁ = { A := (a₂ : P₂.A) × (P₂.B a₂P₁.A), B := fun (a₂a₁ : (a₂ : P₂.A) × (P₂.B a₂P₁.A)) => (u : P₂.B a₂a₁.fst) × P₁.B (a₂a₁.snd u) }
                      Instances For
                        def PFunctor.comp.mk (P₂ : PFunctor.{uA₂, uB₂}) (P₁ : PFunctor.{uA₁, uB₁}) {α : Type v} (x : P₂ (P₁ α)) :
                        (P₂.comp P₁) α

                        Constructor for composition

                        Equations
                        Instances For
                          def PFunctor.comp.get (P₂ : PFunctor.{uA₂, uB₂}) (P₁ : PFunctor.{uA₁, uB₁}) {α : Type v} (x : (P₂.comp P₁) α) :
                          P₂ (P₁ α)

                          Destructor for composition

                          Equations
                          Instances For
                            theorem PFunctor.liftp_iff {P : PFunctor.{uA, uB}} {α : Type u} (p : αProp) (x : P α) :
                            Functor.Liftp p x ∃ (a : P.A) (f : P.B aα), x = a, f ∀ (i : P.B a), p (f i)
                            theorem PFunctor.liftp_iff' {P : PFunctor.{uA, uB}} {α : Type u} (p : αProp) (a : P.A) (f : P.B aα) :
                            Functor.Liftp p a, f ∀ (i : P.B a), p (f i)
                            theorem PFunctor.liftr_iff {P : PFunctor.{uA, uB}} {α : Type u} (r : ααProp) (x y : P α) :
                            Functor.Liftr r x y ∃ (a : P.A) (f₀ : P.B aα) (f₁ : P.B aα), x = a, f₀ y = a, f₁ ∀ (i : P.B a), r (f₀ i) (f₁ i)
                            theorem PFunctor.supp_eq {P : PFunctor.{uA, uB}} {α : Type u} (a : P.A) (f : P.B aα) :