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.A → Type 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 α.

instance PFunctor.instInhabitedPFunctor : Inhabited PFunctor

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

Applying P to an object of Type

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

Applying P to a morphism of Type

instance PFunctor.Obj.inhabited (P : PFunctor) {α : Type u} [Inhabited P.A] [Inhabited α] : Inhabited (PFunctor.Obj P α)

instance PFunctor.instFunctorObj (P : PFunctor) : Functor (PFunctor.Obj P)

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

instance PFunctor.instLawfulFunctorObjInstFunctorObj (P : PFunctor) : LawfulFunctor (PFunctor.Obj P)

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

def PFunctor.W.head {P : PFunctor} : PFunctor.W P → P.A

root element of a W tree

def PFunctor.W.children {P : PFunctor} (x : PFunctor.W P) : PFunctor.B P (PFunctor.W.head x) → PFunctor.W P

children of the root of a W tree

def PFunctor.W.dest {P : PFunctor} : PFunctor.W P → PFunctor.Obj P (PFunctor.W P)

destructor for W-types

def PFunctor.W.mk {P : PFunctor} : PFunctor.Obj P (PFunctor.W P) → PFunctor.W P

constructor for W-types

@[simp]

theorem PFunctor.W.dest_mk {P : PFunctor} (p : PFunctor.Obj P (PFunctor.W P)) : PFunctor.W.dest (PFunctor.W.mk p) = p

@[simp]

theorem PFunctor.W.mk_dest {P : PFunctor} (p : PFunctor.W P) : PFunctor.W.mk (PFunctor.W.dest p) = p

def PFunctor.IdxCat (P : PFunctor) : Type u_1

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

instance PFunctor.IdxCat.inhabited (P : PFunctor) [Inhabited P.A] [Inhabited (PFunctor.B P default)] : Inhabited (PFunctor.IdxCat P)

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

@[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) : PFunctor.Obj.iget (f <$> x) i = f (PFunctor.Obj.iget x i)

def PFunctor.comp (P₂ : PFunctor) (P₁ : PFunctor) : PFunctor

functor composition for polynomial functors

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

constructor for composition

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

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