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 : TypeVec.{u} n → Type u_1) (G : Fin2 n → TypeVec.{u} m → Type u) (v : TypeVec.{u} m) : Type u_1

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

instance MvQPF.Comp.instInhabited {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α : TypeVec.{u} m} [I : Inhabited (F fun (i : Fin2 n) => G i α)] : Inhabited (Comp F G α)

def MvQPF.Comp.mk {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α : TypeVec.{u} m} (x : F fun (i : Fin2 n) => G i α) : Comp F G α

Constructor for functor composition

def MvQPF.Comp.get {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α : TypeVec.{u} m} (x : Comp F G α) : F fun (i : Fin2 n) => G i α

Destructor for functor composition

@[simp]

theorem MvQPF.Comp.mk_get {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α : TypeVec.{u} m} (x : Comp F G α) : Comp.mk x.get = x

@[simp]

theorem MvQPF.Comp.get_mk {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α : TypeVec.{u} m} (x : F fun (i : Fin2 n) => G i α) : (Comp.mk x).get = x

def MvQPF.Comp.map' {n m : ℕ} {G : Fin2 n → TypeVec.{u} m → Type u} {α β : TypeVec.{u} m} (f : α.Arrow β) [(i : Fin2 n) → MvFunctor (G i)] : TypeVec.Arrow (fun (i : Fin2 n) => G i α) fun (i : Fin2 n) => G i β

map operation defined on a vector of functors

def MvQPF.Comp.map {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α β : TypeVec.{u} m} (f : α.Arrow β) [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] : Comp F G α → Comp F G β

The composition of functors is itself functorial

instance MvQPF.Comp.instMvFunctor {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] : MvFunctor (Comp F G)

theorem MvQPF.Comp.map_mk {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α β : TypeVec.{u} m} (f : α.Arrow β) [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] (x : F fun (i : Fin2 n) => G i α) : MvFunctor.map f (Comp.mk x) = Comp.mk (MvFunctor.map (fun (i : Fin2 n) (x : G i α) => MvFunctor.map f x) x)

theorem MvQPF.Comp.get_map {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α β : TypeVec.{u} m} (f : α.Arrow β) [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] (x : Comp F G α) : (MvFunctor.map f x).get = MvFunctor.map (fun (i : Fin2 n) (x : G i α) => MvFunctor.map f x) x.get

instance MvQPF.Comp.inst {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} [MvQPF F] [(i : Fin2 n) → MvQPF (G i)] : MvQPF (Comp F G)