proposition: Lemma closed_under_op_in_image_hom {w : SymbolType σ} (α : Operation A w) (β : Operation B w) (P : OpPreserving f α β) : ClosedUnderOp B in_image_hom β.
proof: Proof. induction w. - exact (tr (α; P)). - intro y. refine (Trunc_rec _). intros [x p]. apply (IHw (α x)). by destruct p. Qed.
imports: HSet Colimits.Quotient Modalities.ReflectiveSubuniverse Classes.interfaces.canonical_names Classes.theory.ua_isomorphic Classes.theory.ua_subalgebra Classes.theory.ua_quotient_algebra