# The composition of QPFs is itself a QPF #

We define composition between one n-ary functor and n m-ary functors and show that it preserves the QPF structure

def MvQPF.Comp {n : } {m : } (F : Type u_1) (G : Fin2 nType u) (v : ) :
Type u_1

Composition of an n-ary functor with n m-ary functors gives us one m-ary functor

Equations
Instances For
instance MvQPF.Comp.instInhabitedComp {n : } {m : } {F : Type u_1} {G : Fin2 nType u} {α : } [I : Inhabited (F fun (i : Fin2 n) => G i α)] :
Equations
• MvQPF.Comp.instInhabitedComp = I
def MvQPF.Comp.mk {n : } {m : } {F : Type u_1} {G : Fin2 nType u} {α : } (x : F fun (i : Fin2 n) => G i α) :
MvQPF.Comp F G α

Constructor for functor composition

Equations
Instances For
def MvQPF.Comp.get {n : } {m : } {F : Type u_1} {G : Fin2 nType u} {α : } (x : MvQPF.Comp F G α) :
F fun (i : Fin2 n) => G i α

Destructor for functor composition

Equations
Instances For
@[simp]
theorem MvQPF.Comp.mk_get {n : } {m : } {F : Type u_1} {G : Fin2 nType u} {α : } (x : MvQPF.Comp F G α) :
@[simp]
theorem MvQPF.Comp.get_mk {n : } {m : } {F : Type u_1} {G : Fin2 nType u} {α : } (x : F fun (i : Fin2 n) => G i α) :
def MvQPF.Comp.map' {n : } {m : } {G : Fin2 nType u} [fG : (i : Fin2 n) → MvFunctor (G i)] {α : } {β : } (f : ) :
TypeVec.Arrow (fun (i : Fin2 n) => G i α) fun (i : Fin2 n) => G i β

map operation defined on a vector of functors

Equations
Instances For
def MvQPF.Comp.map {n : } {m : } {F : Type u_1} [fF : ] {G : Fin2 nType u} [fG : (i : Fin2 n) → MvFunctor (G i)] {α : } {β : } (f : ) :
MvQPF.Comp F G αMvQPF.Comp F G β

The composition of functors is itself functorial

Equations
Instances For
instance MvQPF.Comp.instMvFunctorComp {n : } {m : } {F : Type u_1} [fF : ] {G : Fin2 nType u} [fG : (i : Fin2 n) → MvFunctor (G i)] :
Equations
• MvQPF.Comp.instMvFunctorComp = { map := fun {α β : } => MvQPF.Comp.map }
theorem MvQPF.Comp.map_mk {n : } {m : } {F : Type u_1} [fF : ] {G : Fin2 nType u} [fG : (i : Fin2 n) → MvFunctor (G i)] {α : } {β : } (f : ) (x : F fun (i : Fin2 n) => G i α) :
= MvQPF.Comp.mk (MvFunctor.map (fun (i : Fin2 n) (x : G i α) => ) x)
theorem MvQPF.Comp.get_map {n : } {m : } {F : Type u_1} [fF : ] {G : Fin2 nType u} [fG : (i : Fin2 n) → MvFunctor (G i)] {α : } {β : } (f : ) (x : MvQPF.Comp F G α) :
= MvFunctor.map (fun (i : Fin2 n) (x : G i α) => ) ()
instance MvQPF.Comp.instMvQPFCompInstMvFunctorCompFin2 {n : } {m : } {F : Type u_1} [fF : ] [q : ] {G : Fin2 nType u} [fG : (i : Fin2 n) → MvFunctor (G i)] [q' : (i : Fin2 n) → MvQPF (G i)] :
Equations
• One or more equations did not get rendered due to their size.