Proposition enriched_rezk_completion_ump_faithful : faithful (enriched_precomp E₃ EF). 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.
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.