Projection functors are QPFs. The n-ary projection functors on i is an n-ary
functor F such that F (α₀..αᵢ₋₁, αᵢ, αᵢ₊₁..αₙ₋₁) = αᵢ
@[instance]
Equations
- mvqpf.prj.inhabited i = {default := inhabited.default (v i) _inst_1}
@[instance]
Equations
- mvqpf.prj.mvfunctor i = {map := mvqpf.prj.map i}
Representation function of the qpf instance
Equations
- mvqpf.prj.repr i = λ (x : α i), ⟨punit.star, λ (j : fin2 n) (_x : (mvqpf.prj.P i).B punit.star j), mvqpf.prj.repr._match_1 i x j _x⟩
- mvqpf.prj.repr._match_1 i x j {down := {down := h}} = eq.rec x h
@[instance]
Equations
- mvqpf.prj.mvqpf i = {P := mvqpf.prj.P i, abs := mvqpf.prj.abs i, repr := mvqpf.prj.repr i, abs_repr := _, abs_map := _}