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