# 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 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 u

• B : self.AType u

The child family of types

Instances For
Equations
def PFunctor.Obj (P : PFunctor.{u}) (α : Type v) :
Type (max u u v)

Applying P to an object of Type

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

Applying P to a morphism of Type

Equations
• P.map f x = match x with | a, g => a, f g
Instances For
instance PFunctor.Obj.inhabited (P : PFunctor.{u}) {α : Type v₁} [Inhabited P.A] [] :
Inhabited (P α)
Equations
• = { default := default, default }
Equations
• P.instFunctorObj = { map := , mapConst := fun {α β : Type v} => P.map }
@[simp]
theorem PFunctor.map_eq_map (P : PFunctor.{u}) {α : Type v} {β : 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.{u}) {α : 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.{u}) {α : Type v₁} (x : P α) :
P.map id x = x
@[simp]
theorem PFunctor.map_map (P : PFunctor.{u}) {α : Type v₁} {β : Type v₂} {γ : Type v₃} (f : αβ) (g : βγ) (x : P α) :
P.map g (P.map f x) = P.map (g f) x
Equations
• =

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

Equations
Instances For
def PFunctor.W.head {P : PFunctor.{u}} :
P.WP.A

root element of a W tree

Equations
Instances For
def PFunctor.W.children {P : PFunctor.{u}} (x : P.W) :

children of the root of a W tree

Equations
• x.children = match (motive := (x : P.W) → P.B x.headP.W) x with | WType.mk _a f => f
Instances For
def PFunctor.W.dest {P : PFunctor.{u}} :
P.WP P.W

destructor for W-types

Equations
• x.dest = match x with | WType.mk a f => a, f
Instances For
def PFunctor.W.mk {P : PFunctor.{u}} :
P P.WP.W

constructor for W-types

Equations
Instances For
@[simp]
theorem PFunctor.W.dest_mk {P : PFunctor.{u}} (p : P P.W) :
().dest = p
@[simp]
theorem PFunctor.W.mk_dest {P : PFunctor.{u}} (p : P.W) :
PFunctor.W.mk p.dest = p

Idx identifies a location inside the application of a pfunctor. 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
• P.Idx = ((x : P.A) × P.B x)
Instances For
instance PFunctor.Idx.inhabited (P : PFunctor.{u}) [Inhabited P.A] [Inhabited (P.B default)] :
Inhabited P.Idx
Equations
• = { default := default, default }
def PFunctor.Obj.iget {P : PFunctor.{u}} [DecidableEq P.A] {α : Type u_1} [] (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
• x.iget i = if h : i.fst = x.fst then x.snd (cast i.snd) else default
Instances For
@[simp]
theorem PFunctor.fst_map {P : PFunctor.{u}} {α : Type v₁} {β : Type v₂} (x : P α) (f : αβ) :
(P.map f x).fst = x.fst
@[simp]
theorem PFunctor.iget_map {P : PFunctor.{u}} {α : Type v₁} {β : Type v₂} [DecidableEq P.A] [] [] (x : P α) (f : αβ) (i : P.Idx) (h : i.fst = x.fst) :
(P.map f x).iget i = f (x.iget i)

functor 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.{u}) (P₁ : PFunctor.{u}) {α : Type} (x : P₂ (P₁ α)) :
(P₂.comp P₁) α

constructor for composition

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

destructor for composition

Equations
• PFunctor.comp.get P₂ P₁ x = x.fst.fst, fun (a₂ : P₂.B x.fst.fst) => x.fst.snd a₂, fun (a₁ : P₁.B (x.fst.snd a₂)) => x.snd a₂, a₁
Instances For
theorem PFunctor.liftp_iff {P : PFunctor.{u}} {α : Type u} (p : αProp) (x : P α) :
∃ (a : P.A) (f : P.B aα), x = a, f ∀ (i : P.B a), p (f i)
theorem PFunctor.liftp_iff' {P : PFunctor.{u}} {α : 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.{u}} {α : Type u} (r : ααProp) (x : P α) (y : P α) :
∃ (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.{u}} {α : Type u} (a : P.A) (f : P.B aα) :
Functor.supp a, f = f '' Set.univ