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 n → Type u_1)
(G : fin2 n → typevec m → Type u)
(v : typevec 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 (λ (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}
(x : 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 : ℕ}
{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 : α ⟹ β)
(a : 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 : α ⟹ β)
(x : F (λ (i : fin2 n), G i α)) :
f <$$> mvqpf.comp.mk x = mvqpf.comp.mk ((λ (i : fin2 n) (x : G i α), f <$$> x) <$$> x)
@[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 := _}