proposition: Lemma ishomcomp {σ: signature} {A1 A2 A3: algebra σ} (h1: A1 ↷ A2) (h2: A2 ↷ A3): ishom (h2 s∘ h1).
proof: Proof. red. intros. induction h1 as [h1 ishomh1]. induction h2 as [h2 ishomh2]. cbn. rewrite starcomp. rewrite ishomh1. rewrite ishomh2. apply idpath. Defined.
imports: UniMath.Foundations.All UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Signatures