proposition: Lemma path_path_isomorphism_hom_id_hset `{Univalence} {σ : Signature} (A : Algebra σ) `{IsHSetAlgebra A} : path_isomorphism (hom_id A) = idpath.
proof: 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.
imports: HoTT.Classes.theory.ua_homomorphism HoTT.Types HoTT.Tactics