English
Let L be an algebraic language. Then for any L-structures M,N and any F with FunLike F M N, there is a StrongHomClass L F M N, with map_fun given by the usual HomClass.map_fun and map_rel carried by isEmptyElim.
Русский
Пусть язык L алгебраический. Тогда для любых L-структур M,N и любого F с FunLike F M N существует StrongHomClass L F M N, причём map_fun задаётся как обычная функция HomClass.map_fun, а map_rel тривиально задаётся через isEmptyElim.
LaTeX
$$$[L.IsAlgebraic] \\Rightarrow \\mathrm{StrongHomClass}\\ L\\ F\\ M\\ N$$
Lean4
instance (priority := 100) homClass {F : Type*} [L.Structure M] [L.Structure N] [FunLike F M N]
[StrongHomClass L F M N] : HomClass L F M N
where
map_fun := StrongHomClass.map_fun
map_rel φ _ R x := (StrongHomClass.map_rel φ R x).2
