A $-> A := Build_Homomorphism (fun s (x : A s) => x). End . Arguments {σ} A%_Algebra_scope , {σ} {A}. Section homomorphism_compose. Context {σ} {A B C : Algebra σ}. Global Instance is_homomorphism_compose (g : forall s, B s -> C s) `{!IsHomomorphism g} (f : forall s, A s -> B s) `{!IsHomomorphism f} : IsHomomorphism (fun s => g s o f s). Proof. intros u a. by rewrite <- (oppreserving_hom g), (oppreserving_hom f). Qed.
Require Import