`{Funext} {σ} (A : SetAlgebra σ) : path_setalgebra A A idpath = idpath. Proof. transparent assert (p : (∀ I : IsHSetAlgebra A, path_ishprop I I = idpath)). - intros. apply path_ishprop. - unfold path_setalgebra. by rewrite p. Qed.