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

Equations

• MvQPF.Comp F G v = F fun (i : Fin2 n) => G i v

instance MvQPF.Comp.instInhabitedComp {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 (MvQPF.Comp F G α)

Equations

• MvQPF.Comp.instInhabitedComp = I

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 α) : MvQPF.Comp F G α

Constructor for functor composition

Equations

• MvQPF.Comp.mk x = x

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 : MvQPF.Comp F G α) : F fun (i : Fin2 n) => G i α

Destructor for functor composition

Equations

• MvQPF.Comp.get x = x

@[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 : MvQPF.Comp F G α) : MvQPF.Comp.mk (MvQPF.Comp.get x) = 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 α) : MvQPF.Comp.get (MvQPF.Comp.mk x) = x

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

map operation defined on a vector of functors

Equations

• MvQPF.Comp.map' f _i = MvFunctor.map f

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

The composition of functors is itself functorial

Equations

• MvQPF.Comp.map f = MvFunctor.map fun (_i : Fin2 n) => MvFunctor.map f

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

Equations

• MvQPF.Comp.instMvFunctorComp = { map := fun {α β : TypeVec.{u} m} => MvQPF.Comp.map }

theorem MvQPF.Comp.map_mk {n : ℕ} {m : ℕ} {F : TypeVec.{u} n → Type u_1} [fF : MvFunctor F] {G : Fin2 n → TypeVec.{u} m → Type u} [fG : (i : Fin2 n) → MvFunctor (G i)] {α : TypeVec.{u} m} {β : TypeVec.{u} m} (f : TypeVec.Arrow α β) (x : F fun (i : Fin2 n) => G i α) : MvFunctor.map f (MvQPF.Comp.mk x) = MvQPF.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} [fF : MvFunctor F] {G : Fin2 n → TypeVec.{u} m → Type u} [fG : (i : Fin2 n) → MvFunctor (G i)] {α : TypeVec.{u} m} {β : TypeVec.{u} m} (f : TypeVec.Arrow α β) (x : MvQPF.Comp F G α) : MvQPF.Comp.get (MvFunctor.map f x) = MvFunctor.map (fun (i : Fin2 n) (x : G i α) => MvFunctor.map f x) (MvQPF.Comp.get x)

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

Equations

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