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
@[simp]
theorem
MvQPF.Comp.mk_get
{n : ℕ}
{m : ℕ}
{F : TypeVec n → Type u_1}
{G : Fin2 n → TypeVec m → Type u}
{α : TypeVec m}
(x : MvQPF.Comp F G α)
:
MvQPF.Comp.mk (MvQPF.Comp.get x) = x
@[simp]
theorem
MvQPF.Comp.get_mk
{n : ℕ}
{m : ℕ}
{F : TypeVec n → Type u_1}
{G : Fin2 n → TypeVec m → Type u}
{α : TypeVec m}
(x : F fun i => G i α)
:
MvQPF.Comp.get (MvQPF.Comp.mk x) = x
def
MvQPF.Comp.map'
{n : ℕ}
{m : ℕ}
{G : Fin2 n → TypeVec m → Type u}
[fG : (i : Fin2 n) → MvFunctor (G i)]
{α : TypeVec m}
{β : TypeVec m}
(f : TypeVec.Arrow α β)
:
TypeVec.Arrow (fun i => G i α) fun i => G i β
map operation defined on a vector of functors
Instances For
def
MvQPF.Comp.map
{n : ℕ}
{m : ℕ}
{F : TypeVec n → Type u_1}
[fF : MvFunctor F]
{G : Fin2 n → TypeVec m → Type u}
[fG : (i : Fin2 n) → MvFunctor (G i)]
{α : TypeVec m}
{β : TypeVec m}
(f : TypeVec.Arrow α β)
:
MvQPF.Comp F G α → MvQPF.Comp F G β
The composition of functors is itself functorial
Instances For
theorem
MvQPF.Comp.map_mk
{n : ℕ}
{m : ℕ}
{F : TypeVec n → Type u_1}
[fF : MvFunctor F]
{G : Fin2 n → TypeVec m → Type u}
[fG : (i : Fin2 n) → MvFunctor (G i)]
{α : TypeVec m}
{β : TypeVec m}
(f : TypeVec.Arrow α β)
(x : F fun i => G i α)
:
MvFunctor.map f (MvQPF.Comp.mk x) = MvQPF.Comp.mk (MvFunctor.map (fun i x => MvFunctor.map f x) x)
theorem
MvQPF.Comp.get_map
{n : ℕ}
{m : ℕ}
{F : TypeVec n → Type u_1}
[fF : MvFunctor F]
{G : Fin2 n → TypeVec m → Type u}
[fG : (i : Fin2 n) → MvFunctor (G i)]
{α : TypeVec m}
{β : TypeVec m}
(f : TypeVec.Arrow α β)
(x : MvQPF.Comp F G α)
:
MvQPF.Comp.get (MvFunctor.map f x) = MvFunctor.map (fun i x => MvFunctor.map f x) (MvQPF.Comp.get x)