proposition: Lemma is_closed_under_ops_in_image_hom : IsClosedUnderOps B in_image_hom.
proof: Proof. intro u. eapply closed_under_op_in_image_hom, hom. Qed.
imports: HSet Colimits.Quotient Modalities.ReflectiveSubuniverse Classes.interfaces.canonical_names Classes.theory.ua_isomorphic Classes.theory.ua_subalgebra Classes.theory.ua_quotient_algebra