Theorem isasethom {σ: signature} (A1 A2: algebra σ) (setprop: has_supportsets A2) : isaset (A1 ↷ A2). Proof. red. apply isaset_total2. - apply impred_isaset. intros. apply impred_isaset. intros. apply setprop. - intros. apply isasetaprop. apply isapropishom. exact setprop. Defined.
Require Import UniMath.Foundations.All.