English
If q is a multivariate polynomial functor (MvQPF) for F, then Cofix F inherits a natural MvQPF structure. Its P-component is taken from q.P.mp, its abs-map is given by Quot.mk Mcongr, its repr is Cofix.repr, its abs_repr is Cofix.abs_repr, and abs_map aligns with the underlying map.
Русский
Если q — многовариантный полином-функтор (MvQPF) для F, то Cofix F обладает естественной структурой MvQPF. Компонента P задаётся как q.P.mp, отображение abs задаётся через Quot.mk Mcongr, repr задаётся Cofix.repr, abs_repr — Cofix.abs_repr, а abs_map согласуется с отображением внутри.
LaTeX
$$$\operatorname{MvQPF.Cofix} F$ имеет структуру MvQPF с $P = q.P.mp$, $\operatorname{abs} = \operatorname{Quot.mk} \ \mathrm{Mcongr}$, $\operatorname{repr} = \mathrm{Cofix.repr}$, $\operatorname{abs\_repr} = \mathrm{Cofix.abs\_repr}$, $\operatorname{abs\_map}$ соответствует доказательству.$$
Lean4
instance mvqpfCofix : MvQPF (Cofix F) where
P := q.P.mp
abs := Quot.mk Mcongr
repr := Cofix.repr
abs_repr := Cofix.abs_repr
abs_map := by intros; rfl
