# Multivariate polynomial functors. #

Multivariate polynomial functors are used for defining M-types and W-types. They map a type vector α to the type Σ a : A, B a ⟹ α, with A : Type and B : A → TypeVec n. They interact well with Lean's inductive definitions because they guarantee that occurrences of α are positive.

structure MvPFunctor (n : ) :
Type (u + 1)

multivariate polynomial functors

• A : Type u

• B : self.A

The child family of types

Instances For
def MvPFunctor.Obj {n : } (P : ) (α : ) :

Applying P to an object of Type

Equations
Instances For
instance MvPFunctor.instCoeFunMvPFunctorForAllTypeVecType {n : } :
CoeFun () fun (x : ) => Type u
Equations
• MvPFunctor.instCoeFunMvPFunctorForAllTypeVecType = { coe := MvPFunctor.Obj }
def MvPFunctor.map {n : } (P : ) {α : } {β : } (f : ) :
P αP β

Applying P to a morphism of Type

Equations
• = match x with | { fst := a, snd := g } => { fst := a, snd := }
Instances For
Equations
• MvPFunctor.instInhabitedMvPFunctor = { default := { A := default, B := default } }
instance MvPFunctor.Obj.inhabited {n : } (P : ) {α : } [Inhabited P.A] [(i : Fin2 n) → Inhabited (α i)] :
Inhabited (P α)
Equations
• = { default := { fst := default, snd := fun (x : Fin2 n) (x_1 : P.B default x) => default } }
instance MvPFunctor.instMvFunctorObj {n : } (P : ) :
Equations
• = { map := }
theorem MvPFunctor.map_eq {n : } (P : ) {α : } {β : } (g : ) (a : P.A) (f : TypeVec.Arrow (P.B a) α) :
MvFunctor.map g { fst := a, snd := f } = { fst := a, snd := }
theorem MvPFunctor.id_map {n : } (P : ) {α : } (x : P α) :
MvFunctor.map TypeVec.id x = x
theorem MvPFunctor.comp_map {n : } (P : ) {α : } {β : } {γ : } (f : ) (g : ) (x : P α) :
Equations
• =
def MvPFunctor.const (n : ) (A : Type u) :

Constant functor where the input object does not affect the output

Equations
Instances For
def MvPFunctor.const.mk (n : ) {A : Type u} (x : A) {α : } :
() α

Constructor for the constant functor

Equations
• = { fst := x, snd := fun (x_1 : Fin2 n) (a : ().B x x_1) => }
Instances For
def MvPFunctor.const.get {n : } {A : Type u} {α : } (x : () α) :
A

Destructor for the constant functor

Equations
• = x.fst
Instances For
@[simp]
theorem MvPFunctor.const.get_map {n : } {A : Type u} {α : } {β : } (f : ) (x : () α) :
@[simp]
theorem MvPFunctor.const.get_mk {n : } {A : Type u} {α : } (x : A) :
@[simp]
theorem MvPFunctor.const.mk_get {n : } {A : Type u} {α : } (x : () α) :
def MvPFunctor.comp {n : } {m : } (P : ) (Q : Fin2 n) :

Functor composition on polynomial functors

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MvPFunctor.comp.mk {n : } {m : } {P : } {Q : Fin2 n} {α : } (x : P fun (i : Fin2 n) => (Q i) α) :
() α

Constructor for functor composition

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MvPFunctor.comp.get {n : } {m : } {P : } {Q : Fin2 n} {α : } (x : () α) :
P fun (i : Fin2 n) => (Q i) α

Destructor for functor composition

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MvPFunctor.comp.get_map {n : } {m : } {P : } {Q : Fin2 n} {α : } {β : } (f : ) (x : () α) :
= MvFunctor.map (fun (i : Fin2 n) (x : (Q i) α) => )
@[simp]
theorem MvPFunctor.comp.get_mk {n : } {m : } {P : } {Q : Fin2 n} {α : } (x : P fun (i : Fin2 n) => (Q i) α) :
@[simp]
theorem MvPFunctor.comp.mk_get {n : } {m : } {P : } {Q : Fin2 n} {α : } (x : () α) :
theorem MvPFunctor.liftP_iff {n : } {P : } {α : } (p : i : Fin2 n⦄ → α iProp) (x : P α) :
∃ (a : P.A) (f : TypeVec.Arrow (P.B a) α), x = { fst := a, snd := f } ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
theorem MvPFunctor.liftP_iff' {n : } {P : } {α : } (p : i : Fin2 n⦄ → α iProp) (a : P.A) (f : TypeVec.Arrow (P.B a) α) :
MvFunctor.LiftP p { fst := a, snd := f } ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
theorem MvPFunctor.liftR_iff {n : } {P : } {α : } (r : i : Fin2 n⦄ → α iα iProp) (x : P α) (y : P α) :
∃ (a : P.A) (f₀ : TypeVec.Arrow (P.B a) α) (f₁ : TypeVec.Arrow (P.B a) α), x = { fst := a, snd := f₀ } y = { fst := a, snd := f₁ } ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
theorem MvPFunctor.supp_eq {n : } {P : } {α : } (a : P.A) (f : TypeVec.Arrow (P.B a) α) (i : Fin2 n) :
MvFunctor.supp { fst := a, snd := f } i = f i '' Set.univ
def MvPFunctor.drop {n : } (P : MvPFunctor.{u} (n + 1)) :

Split polynomial functor, get an n-ary functor from an n+1-ary functor

Equations
Instances For

Split polynomial functor, get a univariate functor from an n+1-ary functor

Equations
Instances For
@[reducible]
def MvPFunctor.appendContents {n : } (P : MvPFunctor.{u} (n + 1)) {α : } {β : Type u_1} {a : P.A} (f' : TypeVec.Arrow (().B a) α) (f : ().B aβ) :
TypeVec.Arrow (P.B a) (α ::: β)

append arrows of a polynomial functor application

Equations
Instances For