English
The transport of a QPF structure from F to Quot1 uses a quotient construction: Quot1 is equipped with a QPF structure by applying quotientQPF to F and its mvFunctor, along with the necessary quotient-projected abs and repr.
Русский
Перемещение структуры QPF с F на Quot1 осуществляется через конструкцию квартификации quotientQPF; Quot1 получает структуру QPF через F и mvFunctor, с соответствующими abs и repr.
LaTeX
$$$MvQPF.relQuot : \\forall n F, q : MvQPF F, G, inst, (FG_abs, FG_repr) \\to MvQPF G.$$$
Lean4
/-- `Quot1` is a QPF -/
noncomputable def relQuot : @MvQPF _ (Quot1 R) :=
@quotientQPF n F q _ (MvQPF.Quot1.mvFunctor R Hfunc) (fun x => Quot.mk _ x) Quot.out (fun _x => Quot.out_eq _)
fun _f _x => rfl
