Definition enriched_rezk_completion_ump : adj_equivalence_of_cats (enriched_precomp E₃ EF). Proof. use rad_equivalence_of_cats. - use is_univalent_enriched_functor_cat. apply univalent_category_is_univalent. - apply (enriched_rezk_completion_ump_fully_faithful EF HF₁ HF₂). - exact (enriched_rezk_completion_ump_essentially_surjective EF HF₁ HF₂). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.Precomposition. Require Import UniMath.CategoryTheory.Monoidal.Categories.