Proposition eq_to_enriched_rezk_completion_ump_functor_enrichment_data {x y : C₂} (f : E₂ ⦃ x , y ⦄ --> E₃ ⦃ enriched_rezk_completion_ump_functor x , enriched_rezk_completion_ump_functor y ⦄) (p : ∏ (wx wy : C₁) (ix : z_iso (F wx) x) (iy : z_iso (F wy) y), f = precomp_arr E₂ _ ix · postcomp_arr E₂ _ (inv_from_z_iso iy) · inv_from_z_iso (fully_faithful_enriched_functor_z_iso HF₂ _ _) · EG wx wy · precomp_arr E₃ _ (inv_from_z_iso (enriched_rezk_completion_ump_functor_iso x ix)) · postcomp_arr E₃ _ (enriched_rezk_completion_ump_functor_iso y iy)) : enriched_rezk_completion_ump_functor_enrichment_data x y = f. Proof. exact (!(maponpaths pr1 (pr2 (enriched_rezk_completion_ump_functor_enrichment_iscontr x y) (f ,, p)))). 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.