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

Equations

• MvQPF.Prj i v = v i

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

Equations

• MvQPF.Prj.inhabited i = { default := default }

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

map on functor Prj i

Equations

• MvQPF.Prj.map i f = f i

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

Equations

• MvQPF.Prj.mvfunctor i = { map := MvQPF.Prj.map i }

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

Polynomial representation of the projection functor

Equations

• MvQPF.Prj.P i = { A := PUnit.{u + 1} , B := fun (x : PUnit.{u + 1} ) (j : Fin2 n) => ULift.{u, 0} (PLift (i = j)) }

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

Abstraction function of the QPF instance

Equations

• MvQPF.Prj.abs i x = match x with | { fst := _x, snd := f } => f i { down := { down := ⋯ } }

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

Representation function of the QPF instance

Equations

• MvQPF.Prj.repr i x = { fst := PUnit.unit, snd := fun (j : Fin2 n) (x_1 : (MvQPF.Prj.P i).B PUnit.unit j) => match x_1 with | { down := { down := h } } => h ▸ x }

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

Equations

• MvQPF.Prj.mvqpf i = { P := MvQPF.Prj.P i, abs := MvQPF.Prj.abs i, repr := MvQPF.Prj.repr i, abs_repr := ⋯, abs_map := ⋯ }