Proposition enriched_rezk_completion_ump_full : full (enriched_precomp E₃ EF). Proof. intros G₁ G₂ τ. simple refine (hinhpr (_ ,, _)). - simple refine (_ ,, _). + exact (enriched_rezk_completion_ump_full_nat_trans (pr1 τ)). + exact (enriched_rezk_completion_ump_full_nat_trans_enrichment (pr1 τ) (pr2 τ)). - abstract (use subtypePath ; [ intro ; apply isaprop_nat_trans_enrichment | ] ; use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; pose (enriched_rezk_completion_ump_full_nat_trans_eq (pr1 τ) (F x) x (identity_z_iso _)) as p ; cbn in p ; rewrite !functor_id in p ; rewrite id_left, id_right in p ; exact (!p)). Defined.
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.