Proposition fully_faithful_precomp_inv_left : fully_faithful_precomp_inv · EF x y = identity _. Proof. unfold fully_faithful_precomp_inv. refine (_ @ z_iso_inv_after_z_iso ψ). rewrite !assoc'. apply maponpaths. refine (!(id_right _) @ _). rewrite <- (z_iso_inv_after_z_iso ψ). rewrite !assoc. refine (_ @ id_left _). apply maponpaths_2. rewrite !assoc'. apply z_iso_after_z_iso_inv. 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.Monoidal.Categories.