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
Instances For
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 (MvQPF.Comp F G α)
Equations
- MvQPF.Comp.instInhabited = 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
Instances For
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
- x.get = x
Instances For
@[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 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 α)
:
(MvQPF.Comp.mk x).get = x
def
MvQPF.Comp.map'
{n : ℕ}
{m : ℕ}
{G : Fin2 n → TypeVec.{u} m → Type u}
{α : TypeVec.{u} m}
{β : 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
Equations
- MvQPF.Comp.map' f _i = MvFunctor.map f
Instances For
def
MvQPF.Comp.map
{n : ℕ}
{m : ℕ}
{F : TypeVec.{u} n → Type u_1}
{G : Fin2 n → TypeVec.{u} m → Type u}
{α : TypeVec.{u} m}
{β : TypeVec.{u} m}
(f : α.Arrow β)
[MvFunctor F]
[(i : Fin2 n) → MvFunctor (G i)]
:
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
Instances For
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 (MvQPF.Comp F G)
Equations
- MvQPF.Comp.instMvFunctor = { map := fun {α β : TypeVec.{?u.50} m} (f : α.Arrow β) => MvQPF.Comp.map f }
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}
{β : TypeVec.{u} m}
(f : α.Arrow β)
[MvFunctor F]
[(i : Fin2 n) → MvFunctor (G i)]
(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}
{G : Fin2 n → TypeVec.{u} m → Type u}
{α : TypeVec.{u} m}
{β : TypeVec.{u} m}
(f : α.Arrow β)
[MvFunctor F]
[(i : Fin2 n) → MvFunctor (G i)]
(x : MvQPF.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 (MvQPF.Comp F G)
Equations
- One or more equations did not get rendered due to their size.