Proposition enriched_rezk_completion_ump_full_nat_trans_enrichment : nat_trans_enrichment enriched_rezk_completion_ump_full_nat_trans_data EG₁ EG₂. Proof. use nat_trans_enrichment_via_comp. intros x y. 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_full_nat_trans_eq_alt x wx ix). rewrite (enriched_rezk_completion_ump_full_nat_trans_eq_alt y wy iy). rewrite !precomp_arr_comp, !postcomp_arr_comp. rewrite !assoc. rewrite (functor_enrichment_precomp_arr EG₂ ix). rewrite (functor_enrichment_postcomp_arr EG₁ (inv_from_z_iso iy)). use (cancel_z_iso' (_ ,, postcomp_arr_is_z_iso E₂ _ _ (z_iso_is_z_isomorphism iy))). cbn. rewrite !assoc. rewrite <- postcomp_arr_comp. rewrite z_iso_inv_after_z_iso. rewrite postcomp_arr_id. rewrite id_left. rewrite <- precomp_postcomp_arr. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite <- functor_enrichment_postcomp_arr. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- precomp_postcomp_arr. apply idpath. } refine (_ @ id_left _). rewrite <- precomp_arr_id. rewrite <- (z_iso_after_z_iso_inv ix). rewrite precomp_arr_comp. rewrite !assoc'. apply maponpaths. use (cancel_z_iso' (_ ,, HF₂ wx wy)) ; cbn. rewrite !assoc. etrans. { do 2 apply maponpaths_2. exact (nat_trans_enrichment_to_comp Eτ wx wy). } cbn. rewrite !assoc'. apply maponpaths. rewrite <- precomp_postcomp_arr. rewrite !assoc. apply maponpaths_2. rewrite <- functor_enrichment_precomp_arr. rewrite !assoc'. rewrite <- precomp_postcomp_arr. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. 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.