Theorem isapropishom {σ: signature} {A1 A2: algebra σ} (f: sfun A1 A2) (setprop: has_supportsets A2): isaprop (ishom f). Proof. red. apply impred_isaprop. intros. apply impred_isaprop. intros. apply setprop. Defined.
Require Import UniMath.Foundations.All.