proposition: Proposition enriched_rezk_completion_ump_faithful : faithful (enriched_precomp E₃ EF).
proof: Proof. intros G₁ G₂ τ. use invproofirrelevance. intros θ₁ θ₂. use subtypePath. { intro. apply (homset_property (enriched_functor_category _ _)). } use subtypePath ; [ intro ; apply isaprop_nat_trans_enrichment | ]. use nat_trans_eq ; [ apply homset_property | ]. intro y. assert (H := HF₁ y). revert H. use factor_through_squash. { apply homset_property. } intros x. induction x as [ x f ]. refine (!(id_left _) @ _ @ id_left _). rewrite <- (z_iso_after_z_iso_inv (functor_on_z_iso (pr1 G₁) f)). rewrite !assoc'. apply maponpaths. pose (maponpaths (λ z, pr11 z x · #(pr11 G₂) f) (pr2 θ₁ @ !(pr2 θ₂))) as p. cbn in p. rewrite <- (nat_trans_ax (pr11 θ₁)) in p. rewrite <- (nat_trans_ax (pr11 θ₂)) in p. exact p. Qed.
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