proposition: Lemma oppreserving_compose (g : ∀ s, B s → C s) `{!IsHomomorphism g} (f : ∀ s, A s → B s) `{!IsHomomorphism f} {w : SymbolType σ} (α : Operation A w) (β : Operation B w) (γ : Operation C w) (G : OpPreserving g β γ) (F : OpPreserving f α β) : OpPreserving (λ s, g s o f s) α γ.
proof: Proof. induction w; simpl in *. - by path_induction. - intro x. now apply (IHw _ (β (f _ x))). Defined.
imports: HoTT.Classes.interfaces.ua_setalgebra HoTT.Types HoTT.Tactics