English
IsPrecongr r expresses that r is compatible with M-congruence via the abs/dest operation.
Русский
IsPrecongr r задаёт совместимость r с конгруэнцией M через операции abs/dest.
LaTeX
$$$$ \\mathrm{IsPrecongr}\\; r := \\forall x,y,\\ r\\ x\\ y \\Rightarrow \\mathrm{abs}(\\mathrm{appendFun}(\\mathrm{id}, \\mathrm{Quot.mk} r) \\llap{\\$} \\mathrm{dest} q.P\\ x) = \\mathrm{abs}(\\mathrm{appendFun}(\\mathrm{id}, \\mathrm{Quot.mk} r) \\llap{\\$} \\mathrm{dest} q.P\\ y). $$$$
Lean4
/-- Characterization of desirable equivalence relations on M-types -/
def IsPrecongr {α : TypeVec n} (r : q.P.M α → q.P.M α → Prop) : Prop :=
∀ ⦃x y⦄, r x y → abs (appendFun id (Quot.mk r) <$$> M.dest q.P x) = abs (appendFun id (Quot.mk r) <$$> M.dest q.P y)
