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

  The head type

• B : self.A → Type u

  The child family of types

instance PFunctor.instInhabitedPFunctor : Inhabited PFunctor.{u_1}

Equations

• PFunctor.instInhabitedPFunctor = { default := { A := default, B := default } }

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 → α))

instance PFunctor.instCoeFunPFunctorForAllTypeType : CoeFun PFunctor.{u} fun (x : PFunctor.{u}) => Type v → Type (max u v)

Equations

• PFunctor.instCoeFunPFunctorForAllTypeType = { coe := PFunctor.Obj }

def PFunctor.map (P : PFunctor.{u}) {α : Type v₁} {β : Type v₂} (f : α → β) : ↑P α → ↑P β

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.{u}) {α : Type v₁} [Inhabited P.A] [Inhabited α] : Inhabited (↑P α)

Equations

• PFunctor.Obj.inhabited P = { default := { fst := default, snd := default } }

instance PFunctor.instFunctorObj (P : PFunctor.{u}) : Functor ↑P

Equations

• PFunctor.instFunctorObj P = { map := @PFunctor.map P, mapConst := fun {α β : Type v} => PFunctor.map P ∘ Function.const β }

@[simp]

theorem PFunctor.map_eq_map (P : PFunctor.{u}) {α : Type v} {β : Type v} (f : α → β) (x : ↑P α) : f <$> x = PFunctor.map P 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 → α) : PFunctor.map P f { fst := a, snd := g } = { fst := a, snd := f ∘ g }

@[simp]

theorem PFunctor.id_map (P : PFunctor.{u}) {α : Type v₁} (x : ↑P α) : PFunctor.map P id x = x

@[simp]

theorem PFunctor.map_map (P : PFunctor.{u}) {α : Type v₁} {β : Type v₂} {γ : Type v₃} (f : α → β) (g : β → γ) (x : ↑P α) : PFunctor.map P g (PFunctor.map P f x) = PFunctor.map P (g ∘ f) x

instance PFunctor.instLawfulFunctorObjInstFunctorObj (P : PFunctor.{u}) : LawfulFunctor ↑P

Equations

• ⋯ = ⋯

def PFunctor.W (P : PFunctor.{u}) : Type u

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

Equations

• PFunctor.W P = WType P.B

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

root element of a W tree

Equations

• PFunctor.W.head x = match x with | WType.mk a _f => a

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

children of the root of a W tree

Equations

• PFunctor.W.children x = match (motive := (x : PFunctor.W P) → P.B (PFunctor.W.head x) → PFunctor.W P) x with | WType.mk _a f => f

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

destructor for W-types

Equations

• PFunctor.W.dest x = match x with | WType.mk a f => { fst := a, snd := f }

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

constructor for W-types

Equations

• PFunctor.W.mk x = match x with | { fst := a, snd := f } => WType.mk a f

@[simp]

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

@[simp]

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

def PFunctor.Idx (P : PFunctor.{u}) : Type u

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

• PFunctor.Idx P = ((x : P.A) × P.B x)

instance PFunctor.Idx.inhabited (P : PFunctor.{u}) [Inhabited P.A] [Inhabited (P.B default)] : Inhabited (PFunctor.Idx P)

Equations

• PFunctor.Idx.inhabited P = { default := { fst := default, snd := default } }

def PFunctor.Obj.iget {P : PFunctor.{u}} [DecidableEq P.A] {α : Type u_1} [Inhabited α] (x : ↑P α) (i : PFunctor.Idx P) : α

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

Equations

• PFunctor.Obj.iget x i = if h : i.fst = x.fst then x.snd (cast ⋯ i.snd) else default

@[simp]

theorem PFunctor.fst_map {P : PFunctor.{u}} {α : Type v₁} {β : Type v₂} (x : ↑P α) (f : α → β) : (PFunctor.map P f x).fst = x.fst

@[simp]

theorem PFunctor.iget_map {P : PFunctor.{u}} {α : Type v₁} {β : Type v₂} [DecidableEq P.A] [Inhabited α] [Inhabited β] (x : ↑P α) (f : α → β) (i : PFunctor.Idx P) (h : i.fst = x.fst) : PFunctor.Obj.iget (PFunctor.map P f x) i = f (PFunctor.Obj.iget x i)

def PFunctor.comp (P₂ : PFunctor.{u}) (P₁ : PFunctor.{u}) : PFunctor.{u}

functor composition for polynomial functors

Equations

• PFunctor.comp P₂ 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) }

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

constructor for composition

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.comp.get (P₂ : PFunctor.{u}) (P₁ : PFunctor.{u}) {α : Type} (x : ↑(PFunctor.comp P₂ P₁) α) : ↑P₂ (↑P₁ α)

destructor for composition

Equations

• One or more equations did not get rendered due to their size.

theorem PFunctor.liftp_iff {P : PFunctor.{u}} {α : Type u} (p : α → Prop) (x : ↑P α) : Functor.Liftp p x ↔ ∃ (a : P.A) (f : P.B a → α), x = { fst := a, snd := 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 { fst := a, snd := f } ↔ ∀ (i : P.B a), p (f i)

theorem PFunctor.liftr_iff {P : PFunctor.{u}} {α : Type u} (r : α → α → Prop) (x : ↑P α) (y : ↑P α) : Functor.Liftr r x y ↔ ∃ (a : P.A) (f₀ : P.B a → α) (f₁ : P.B a → α), x = { fst := a, snd := f₀ } ∧ y = { fst := a, snd := 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 { fst := a, snd := f } = f '' Set.univ