proposition: Theorem isasethom {σ: signature} (A1 A2: algebra σ) (setprop: has_supportsets A2) : isaset (A1 ↷ A2).
proof: Proof. red. apply isaset_total2. - apply impred_isaset. intros. apply impred_isaset. intros. apply setprop. - intros. apply isasetaprop. apply isapropishom. exact setprop. Defined.
imports: UniMath.Foundations.All UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Signatures