Definition enrichment_data_hom_path {C : category} {V : monoidal_cat} (HV : is_univalent V) (E₁ E₂ : enrichment_data C V) : E₁ ╝ E₂ ≃ enrichment_data_hom_path_help E₁ E₂. Proof. use (weqbandf (enrichment_data_hom_weq HV E₁ E₂)). intros p. induction E₁ as [ M₁ E₁ ]. induction E₂ as [ M₂ E₂ ]. cbn in *. induction p. cbn. use weqimplimpl. - intro p. induction p. repeat split ; intros. + rewrite id_right. apply idpath. + rewrite id_right. rewrite tensor_id_id. rewrite id_left. apply idpath. + apply id_right. + rewrite id_right. apply idpath. - intros p. repeat (use pathsdirprod). + use funextsec ; intro x. pose (pr1 p x) as q. rewrite id_right in q. exact q. + use funextsec ; intro x. use funextsec ; intro y. use funextsec ; intro z. pose (pr12 p x y z) as q. rewrite id_right in q. rewrite tensor_id_id in q. rewrite id_left in q. exact q. + use funextsec ; intro x. use funextsec ; intro y. use funextsec ; intro f. pose (pr122 p x y f) as q. cbn in q. rewrite id_right in q. exact q. + use funextsec ; intro x. use funextsec ; intro y. use funextsec ; intro f. pose (pr222 p x y f) as q. cbn in q. rewrite id_right in q. exact q. - repeat (apply isaset_dirprod) ; repeat (use impred_isaset ; intro) ; apply homset_property. - repeat (apply isapropdirprod) ; repeat (use impred ; intro) ; apply homset_property. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import MonoidalNotations.