Definition make_hSetalgebra {σ : signature} {A: algebra σ} (setproperty: has_supportsets A): hSetalgebra σ := ((λ s : sorts σ, make_hSet (support A s) (setproperty s)),, ops A).
Require Import UniMath.Foundations.All.