proposition: Lemma path_setalgebra_1 `{Funext} {σ} (A : SetAlgebra σ) : path_setalgebra A A idpath = idpath.
proof: Proof. transparent assert (p : (∀ I : IsHSetAlgebra A, path_ishprop I I = idpath)). - intros. apply path_ishprop. - unfold path_setalgebra. by rewrite p. Qed.
imports: HoTT.Classes.interfaces.ua_algebra