Proposition enriched_rezk_completion_ump_functor_enrichment_laws : is_functor_enrichment enriched_rezk_completion_ump_functor_enrichment_data. Proof. repeat split. - intro x. assert (H := HF₁ x). revert H. use factor_through_squash ; [ apply homset_property | ]. intros w. induction w as [ w i ]. rewrite (enriched_rezk_completion_ump_functor_enrichment_eq i i). rewrite !assoc. rewrite enriched_id_precomp_arr. rewrite enriched_from_arr_postcomp. rewrite z_iso_inv_after_z_iso. rewrite enriched_from_arr_id. rewrite <- (functor_enrichment_id EF). rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. do 3 apply maponpaths_2. exact (z_iso_inv_after_z_iso (fully_faithful_enriched_functor_z_iso HF₂ w w)). } rewrite id_left. rewrite !assoc. rewrite functor_enrichment_id. rewrite enriched_id_precomp_arr. rewrite enriched_from_arr_postcomp. rewrite z_iso_after_z_iso_inv. rewrite enriched_from_arr_id. apply idpath. - intros x y z ; cbn. assert (H := HF₁ x). revert H. use factor_through_squash ; [ apply homset_property | ]. intros wx. induction wx as [ wx ix ]. assert (H := HF₁ y). revert H. use factor_through_squash ; [ apply homset_property | ]. intros wy. induction wy as [ wy iy ]. assert (H := HF₁ z). revert H. use factor_through_squash ; [ apply homset_property | ]. intros wz. induction wz as [ wz iz ]. rewrite (enriched_rezk_completion_ump_functor_enrichment_eq ix iz). rewrite (enriched_rezk_completion_ump_functor_enrichment_eq ix iy). rewrite (enriched_rezk_completion_ump_functor_enrichment_eq iy iz). etrans. { rewrite !assoc. rewrite enriched_comp_precomp_arr. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite enriched_comp_postcomp_arr. apply idpath. } rewrite !assoc. rewrite <- tensor_split. apply idpath. } refine (_ @ id_left _). rewrite <- tensor_id_id. rewrite <- postcomp_arr_id. rewrite <- precomp_arr_id. rewrite <- (z_iso_after_z_iso_inv iz). rewrite <- (z_iso_after_z_iso_inv ix). rewrite postcomp_arr_comp. rewrite precomp_arr_comp. rewrite tensor_comp_mor. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_mor. refine (!_). etrans. { apply maponpaths_2. etrans. { apply maponpaths_2. rewrite !assoc. rewrite <- precomp_postcomp_arr. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- postcomp_arr_comp. rewrite z_iso_inv_after_z_iso. rewrite postcomp_arr_id. rewrite id_left. apply idpath. } apply maponpaths. rewrite !assoc. rewrite <- precomp_arr_comp. rewrite z_iso_inv_after_z_iso. rewrite precomp_arr_id. rewrite id_left. apply idpath. } etrans. { rewrite !assoc'. rewrite tensor_comp_mor. apply idpath. } refine (_ @ id_left _). rewrite <- tensor_id_id. refine (!_). etrans. { apply maponpaths_2. etrans. { apply maponpaths_2. rewrite <- precomp_arr_id. rewrite <- (z_iso_after_z_iso_inv iy). rewrite precomp_arr_comp. apply idpath. } rewrite <- postcomp_arr_id. rewrite <- (z_iso_after_z_iso_inv iy). rewrite postcomp_arr_comp. rewrite tensor_comp_mor. apply idpath. } rewrite !assoc'. apply maponpaths. etrans. { rewrite !assoc. do 4 apply maponpaths_2. rewrite tensor_split. rewrite !assoc'. rewrite precomp_postcomp_arr_assoc. rewrite !assoc. rewrite <- tensor_comp_id_l. rewrite <- postcomp_arr_comp. rewrite z_iso_inv_after_z_iso. rewrite postcomp_arr_id. rewrite tensor_id_id. apply id_left. } rewrite tensor_comp_mor. refine (!(id_left _) @ _). rewrite !assoc'. rewrite <- tensor_id_id. rewrite <- (z_iso_after_z_iso_inv (fully_faithful_enriched_functor_z_iso HF₂ wy wz)). rewrite <- (z_iso_after_z_iso_inv (fully_faithful_enriched_functor_z_iso HF₂ wx wy)). cbn. rewrite tensor_comp_mor. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- functor_enrichment_comp. etrans. { rewrite !assoc'. apply maponpaths. rewrite !assoc. do 3 apply maponpaths_2. apply (z_iso_inv_after_z_iso (fully_faithful_enriched_functor_z_iso HF₂ wx wz)). } rewrite id_left. rewrite !assoc. rewrite functor_enrichment_comp. rewrite !assoc'. rewrite tensor_comp_mor. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite enriched_comp_precomp_arr. rewrite !assoc'. rewrite enriched_comp_postcomp_arr. rewrite !assoc. rewrite <- tensor_split. refine (!_). etrans. { do 2 apply maponpaths_2. apply precomp_postcomp_arr. } rewrite tensor_comp_mor. rewrite !assoc'. apply maponpaths. rewrite tensor_split. rewrite !assoc'. rewrite precomp_postcomp_arr_assoc. rewrite !assoc. rewrite <- tensor_comp_id_l. rewrite <- postcomp_arr_comp. rewrite z_iso_inv_after_z_iso. rewrite postcomp_arr_id. rewrite tensor_id_id. apply id_left. - intros x y f ; cbn. assert (H := HF₁ x). revert H. use factor_through_squash ; [ apply homset_property | ]. intros wx. induction wx as [ wx ix ]. assert (H := HF₁ y). revert H. use factor_through_squash ; [ apply homset_property | ]. intros wy. induction wy as [ wy iy ]. rewrite (enriched_rezk_completion_ump_functor_enrichment_eq ix iy). rewrite !assoc. rewrite enriched_from_arr_precomp. rewrite enriched_from_arr_postcomp. pose (j := invmap (make_weq _ (F_fully_faithful _ _)) (ix · f · inv_from_z_iso iy)). assert (ix · f · inv_from_z_iso iy = #F j) as q. { refine (!_). apply (homotweqinvweq (make_weq _ (F_fully_faithful _ _))). } rewrite q. rewrite (functor_enrichment_from_arr EF). refine (!_). etrans. { rewrite !assoc'. apply maponpaths. rewrite !assoc. do 3 apply maponpaths_2. apply (z_iso_inv_after_z_iso (fully_faithful_enriched_functor_z_iso HF₂ _ _)). } rewrite id_left. rewrite !assoc. rewrite <- functor_enrichment_from_arr. rewrite enriched_from_arr_precomp. rewrite enriched_from_arr_postcomp. apply maponpaths. rewrite !assoc'. etrans. { apply maponpaths. refine (!(enriched_rezk_completion_ump_functor_mor_eq f j ix iy _)). rewrite <- q. rewrite !assoc'. rewrite z_iso_after_z_iso_inv. rewrite id_right. apply idpath. } rewrite !assoc. rewrite z_iso_after_z_iso_inv. apply id_left. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.FullyFaithful. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.Precomposition. Require Import UniMath.CategoryTheory.Monoidal.Categories.