`{Funext} {σ} (A B : SetAlgebra σ) (p : algebra_setalgebra A = algebra_setalgebra B) : A = B. 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.