Projection functors are QPFs. The n-ary projection functors on i is an n-ary functor F such that F (α₀..αᵢ₋₁, αᵢ, αᵢ₊₁..αₙ₋₁) = αᵢ

def MvQPF.Prj {n : ℕ} (i : Fin2 n) (v : TypeVec.{u} n) : Type u

The projection i functor

@[implicit_reducible]

instance MvQPF.Prj.inhabited {n : ℕ} (i : Fin2 n) {v : TypeVec.{u} n} [Inhabited (v i)] : Inhabited (Prj i v)

def MvQPF.Prj.map {n : ℕ} (i : Fin2 n) ⦃α : TypeVec.{u_1} n⦄ ⦃β : TypeVec.{u_2} n⦄ (f : α.Arrow β) : Prj i α → Prj i β

map on functor Prj i

@[implicit_reducible]

instance MvQPF.Prj.mvfunctor {n : ℕ} (i : Fin2 n) : MvFunctor (Prj i)

def MvQPF.Prj.P {n : ℕ} (i : Fin2 n) : MvPFunctor.{u} n

Polynomial representation of the projection functor

def MvQPF.Prj.abs {n : ℕ} (i : Fin2 n) ⦃α : TypeVec.{u_1} n⦄ : ↑(P i) α → Prj i α

Abstraction function of the QPF instance

def MvQPF.Prj.repr {n : ℕ} (i : Fin2 n) ⦃α : TypeVec.{u_1} n⦄ : Prj i α → ↑(P i) α

Representation function of the QPF instance

@[implicit_reducible]

instance MvQPF.Prj.mvqpf {n : ℕ} (i : Fin2 n) : MvQPF (Prj i)