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
Composition of an n-ary functor with n m-ary
functors gives us one m-ary functor
Equations
- mvqpf.comp F G v = F (λ (i : fin2 n), G i v)
@[instance]
def
mvqpf.comp.inhabited
{n m : ℕ}
{F : typevec n → Type u_1}
{G : fin2 n → typevec m → Type u}
{α : typevec m}
[I : inhabited (F (λ (i : fin2 n), G i α))] :
inhabited (mvqpf.comp F G α)
Equations
def
mvqpf.comp.mk
{n m : ℕ}
{F : typevec n → Type u_1}
{G : fin2 n → typevec m → Type u}
{α : typevec m} :
F (λ (i : fin2 n), G i α) → mvqpf.comp F G α
Constructor for functor composition
Equations
- mvqpf.comp.mk x = x
@[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 x.get = x
def
mvqpf.comp.map'
{n m : ℕ}
{G : fin2 n → typevec m → Type u}
[fG : Π (i : fin2 n), mvfunctor (G i)]
{α β : typevec m} :
α.arrow β → typevec.arrow (λ (i : fin2 n), G i α) (λ (i : fin2 n), G i β)
map operation defined on a vector of functors
Equations
- mvqpf.comp.map' f = λ (i : fin2 n), mvfunctor.map f
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} :
α.arrow β → mvqpf.comp F G α → mvqpf.comp F G β
The composition of functors is itself functorial
Equations
- mvqpf.comp.map f = mvfunctor.map (λ (i : fin2 n), mvfunctor.map f)
@[instance]
def
mvqpf.comp.mvfunctor
{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)] :
mvfunctor (mvqpf.comp F G)
Equations
- mvqpf.comp.mvfunctor = {map := λ (α β : typevec m), mvqpf.comp.map}
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}
(f : α.arrow β)
(x : F (λ (i : fin2 n), G i α)) :
mvfunctor.map f (mvqpf.comp.mk x) = mvqpf.comp.mk (mvfunctor.map (λ (i : fin2 n) (x : G i α), 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}
(f : α.arrow β)
(x : mvqpf.comp F G α) :
(mvfunctor.map f x).get = mvfunctor.map (λ (i : fin2 n) (x : G i α), mvfunctor.map f x) x.get
@[instance]
def
mvqpf.comp.mvqpf
{n m : ℕ}
{F : typevec n → Type u_1}
[fF : mvfunctor F]
[q : mvqpf F]
{G : fin2 n → typevec m → Type u}
[fG : Π (i : fin2 n), mvfunctor (G i)]
[q' : Π (i : fin2 n), mvqpf (G i)] :
mvqpf (mvqpf.comp F G)
Equations
- mvqpf.comp.mvqpf = {P := (mvqpf.P F).comp (λ (i : fin2 n), mvqpf.P (G i)), abs := λ (α : typevec m), mvqpf.comp.mk ∘ mvfunctor.map (λ (i : fin2 n), mvqpf.abs) ∘ mvqpf.abs ∘ mvpfunctor.comp.get, repr := λ (α : typevec m), mvpfunctor.comp.mk ∘ mvqpf.repr ∘ mvfunctor.map (λ (i : fin2 n), mvqpf.repr) ∘ mvqpf.comp.get, abs_repr := _, abs_map := _}