proposition: Lemma ishomid {σ: signature} (A: algebra σ): ishom (idsfun A).
proof: Proof. red. intros. rewrite staridfun. apply idpath. Defined.
imports: UniMath.Foundations.All UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Signatures