Projection functors are QPFs. The n
-ary projection functors on i
is an n
-ary
functor F
such that F (α₀..αᵢ₋₁, αᵢ, αᵢ₊₁..αₙ₋₁) = αᵢ
Polynomial representation of the projection functor
Instances For
def
MvQPF.Prj.abs
{n : ℕ}
(i : Fin2 n)
⦃α : TypeVec n⦄
:
MvPFunctor.Obj (MvQPF.Prj.P i) α → MvQPF.Prj i α
Abstraction function of the QPF
instance
Instances For
def
MvQPF.Prj.repr
{n : ℕ}
(i : Fin2 n)
⦃α : TypeVec n⦄
:
MvQPF.Prj i α → MvPFunctor.Obj (MvQPF.Prj.P i) α
Representation function of the QPF
instance