proposition: Theorem isapropishom {σ: signature} {A1 A2: algebra σ} (f: sfun A1 A2) (setprop: has_supportsets A2): isaprop (ishom f).
proof: Proof. red. apply impred_isaprop. intros. apply impred_isaprop. intros. apply setprop. Defined.
imports: UniMath.Foundations.All UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Signatures