# 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 child family of types

B : AType u

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
Equations
def PFunctor.Obj (P : PFunctor) (α : Type u_2) :
Type (maxu_1u_2u_1)

Applying P to an object of Type

Equations
• = ((x : P.A) × (α))
def PFunctor.map (P : PFunctor) {α : Type u_2} {β : Type u_3} (f : αβ) :

Applying P to a morphism of Type

Equations
• PFunctor.map P f x = match x with | { fst := a, snd := g } => { fst := a, snd := f g }
instance PFunctor.Obj.inhabited (P : PFunctor) {α : Type u} [inst : Inhabited P.A] [inst : ] :
Equations
• = { default := { fst := default, snd := default } }
Equations
• = { map := , mapConst := fun {α β} => }
theorem PFunctor.map_eq (P : PFunctor) {α : Type u_1} {β : Type u_1} (f : αβ) (a : P.A) (g : α) :
f <$> { fst := a, snd := g } = { fst := a, snd := f g } theorem PFunctor.id_map (P : PFunctor) {α : Type u_1} (x : ) : id <$> x = id x
theorem PFunctor.comp_map (P : PFunctor) {α : Type u_1} {β : Type u_1} {γ : Type u_1} (f : αβ) (g : βγ) (x : ) :
(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 Equations def PFunctor.W.head {P : PFunctor} : P.A root element of a W tree Equations def PFunctor.W.children {P : PFunctor} (x : ) : children of the root of a W tree Equations • = match (motive := (x : ) → ) x with | WType.mk _a f => f def PFunctor.W.dest {P : PFunctor} : destructor for W-types Equations • = match x with | WType.mk a f => { fst := a, snd := f } def PFunctor.W.mk {P : PFunctor} : constructor for W-types Equations • = match x with | { fst := a, snd := f } => WType.mk a f @[simp] theorem PFunctor.W.dest_mk {P : PFunctor} (p : ) : @[simp] theorem PFunctor.W.mk_dest {P : PFunctor} (p : ) : 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 Equations • = ((x : P.A) × ) instance PFunctor.IdxCat.inhabited (P : PFunctor) [inst : Inhabited P.A] [inst : Inhabited (PFunctor.B P default)] : Equations • = { default := { fst := default, snd := default } } def PFunctor.Obj.iget {P : PFunctor} [inst : DecidableEq P.A] {α : Type u_2} [inst : ] (x : ) (i : ) : α x.iget i takes the component of x designated by i if any is or returns a default value Equations @[simp] theorem PFunctor.fst_map {P : PFunctor} {α : Type u} {β : Type u} (x : ) (f : αβ) : (f <$> x).fst = x.fst
@[simp]
theorem PFunctor.iget_map {P : PFunctor} [inst : DecidableEq P.A] {α : Type u} {β : Type u} [inst : ] [inst : ] (x : ) (f : αβ) (i : ) (h : i.fst = x.fst) :
PFunctor.Obj.iget (f <\$> x) i = f ()
def PFunctor.comp (P₂ : PFunctor) (P₁ : PFunctor) :

functor composition for polynomial functors

Equations
• One or more equations did not get rendered due to their size.
def PFunctor.comp.mk (P₂ : PFunctor) (P₁ : PFunctor) {α : Type} (x : PFunctor.Obj P₂ (PFunctor.Obj P₁ α)) :

constructor for composition

Equations
• One or more equations did not get rendered due to their size.
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

Equations
• One or more equations did not get rendered due to their size.
theorem PFunctor.liftp_iff {P : PFunctor} {α : Type u} (p : αProp) (x : ) :
a f, x = { fst := a, snd := f } ((i : ) → p (f i))
theorem PFunctor.liftp_iff' {P : PFunctor} {α : Type u} (p : αProp) (a : P.A) (f : α) :
Functor.Liftp p { fst := a, snd := f } (i : ) → p (f i)
theorem PFunctor.liftr_iff {P : PFunctor} {α : Type u} (r : ααProp) (x : ) (y : ) :
a f₀ f₁, x = { fst := a, snd := f₀ } y = { fst := a, snd := f₁ } ((i : ) → r (f₀ i) (f₁ i))
theorem PFunctor.supp_eq {P : PFunctor} {α : Type u} (a : P.A) (f : α) :
Functor.supp { fst := a, snd := f } = f '' Set.univ