proposition: Lemma path_setalgebra `{Funext} {σ} (A B : SetAlgebra σ) (p : algebra_setalgebra A = algebra_setalgebra B) : A = B.
proof: Proof. destruct A as [A AH], B as [B BH]. cbn in *. transparent assert (a : (p#AH = BH)) by apply path_ishprop. by path_induction. Defined.
imports: HoTT.Classes.interfaces.ua_algebra