English
The constant multivariate functor Cmv has an MvQPF structure with P from the base const functor, abs as get, repr as mk, and coherence maps given by existing lemmas.
Русский
У константного мультфункторa Cmv имеется структура MvQPF, где P берётся от базового константного функторa, abs — get, repr — mk, а остальные отображения согласованы с существующими леммами.
LaTeX
$$$\mathrm{MvQPF}.mvqpf: \mathrm{MvQPF} (\mathrm{Const}\; n\; A)$ with $P = \mathrm{MvPFunctor.const}\; n\; A$, $abs = \mathrm{MvPFunctor.const.get}$, $repr = \mathrm{MvPFunctor.const.mk}$, $abs\_repr = \mathrm{const.get_mk}$, $abs\_map = \mathrm{const.get_map}$.$$
Lean4
instance mvqpf : @MvQPF _ (Const n A) where
P := MvPFunctor.const n A
abs x := MvPFunctor.const.get x
repr x := MvPFunctor.const.mk n x
abs_repr := fun _ => const.get_mk _
abs_map := fun _ => const.get_map _
