Proposition enriched_rezk_completion_ump_functor_laws : is_functor enriched_rezk_completion_ump_functor_data. Proof. split. - intro x ; cbn. use eq_to_enriched_rezk_completion_ump_functor_mor. intros w₁ w₂ h i₁ i₂ p. rewrite id_right in p. rewrite id_right. rewrite (enriched_rezk_completion_ump_functor_eq x i₁ i₂ _ p). apply idpath. - intros x y z f g ; cbn. use eq_to_enriched_rezk_completion_ump_functor_mor. intros wx wz h ix iz p. assert (H := HF₁ y). revert H. use factor_through_squash ; [ apply homset_property | ]. intros wy. induction wy as [ wy iy ]. pose (j := invmap (make_weq _ (F_fully_faithful _ _)) (ix · f · inv_from_z_iso iy)). assert (# F j · iy = ix · f) as q. { etrans. { apply maponpaths_2. apply (homotweqinvweq (make_weq _ (F_fully_faithful _ _))). } rewrite !assoc'. rewrite z_iso_after_z_iso_inv. rewrite id_right. apply idpath. } pose (k := invmap (make_weq _ (F_fully_faithful _ _)) (iy · g · inv_from_z_iso iz)). assert (# F k · iz = iy · g) as r. { etrans. { apply maponpaths_2. apply (homotweqinvweq (make_weq _ (F_fully_faithful _ _))). } rewrite !assoc'. rewrite z_iso_after_z_iso_inv. rewrite id_right. apply idpath. } rewrite !assoc. etrans. { apply maponpaths_2. exact (enriched_rezk_completion_ump_functor_mor_eq f j ix iy q). } rewrite !assoc'. etrans. { apply maponpaths. exact (enriched_rezk_completion_ump_functor_mor_eq g k iy iz r). } rewrite !assoc. apply maponpaths_2. rewrite <- functor_comp. apply maponpaths. use (invmaponpathsweq (weq_from_fully_faithful F_fully_faithful _ _)). cbn. rewrite functor_comp. etrans. { apply maponpaths_2. apply (homotweqinvweq (make_weq _ (F_fully_faithful _ _))). } etrans. { apply maponpaths. apply (homotweqinvweq (make_weq _ (F_fully_faithful _ _))). } refine (_ @ id_right _). rewrite <- (z_iso_inv_after_z_iso iz). rewrite !assoc. apply maponpaths_2. rewrite p. rewrite !assoc'. do 2 apply maponpaths. 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.