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 (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 : α.Arrow β) : Prj i α → Prj i β

map on functor Prj i

Equations

• MvQPF.Prj.map i f = f i

instance MvQPF.Prj.mvfunctor {n : ℕ} (i : Fin2 n) : MvFunctor (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.12 + 1}, B := fun (x : PUnit.{?u.12 + 1}) (j : Fin2 n) => ULift.{?u.12, 0} (PLift (i = j)) }

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

Abstraction function of the QPF instance

Equations

• MvQPF.Prj.abs i ⟨_x, f⟩ = f i { down := { down := ⋯ } }

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

Representation function of the QPF instance

Equations

• MvQPF.Prj.repr i x = ⟨PUnit.unit, 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 (Prj i)

Equations

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