proposition: Proposition enriched_rezk_completion_ump_full : full (enriched_precomp E₃ EF).
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.FullyFaithful UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory UniMath.CategoryTheory.EnrichedCats.Examples.Precomposition UniMath.CategoryTheory.Monoidal.Categories