`{Univalence} {σ : Signature} (A : Algebra σ) `{IsHSetAlgebra A} : path_isomorphism (hom_id A) = idpath. Proof. apply path_path_hset_algebra. rewrite path_ap_carriers_path_algebra. apply (paths_ind (λ s, idpath) (λ f _, path_forall A A f = idpath)). - apply path_forall_1. - intros. funext s. symmetry. rewrite (path_ishprop _ (isequiv_idmap (A s))). apply path_universe_1. Qed.
Require Import Import isomorphic_notations.