{w : SymbolType σ} (α : Operation A w) (β : Operation B w) (P : OpPreserving f α β) : ClosedUnderOp B in_image_hom β. Proof. induction w. - exact (tr (α; P)). - intro y. refine (Trunc_rec _). intros [x p]. apply (IHw (α x)). by destruct p. Qed.
Require Import Import