proposition: Proposition fully_faithful_precomp_inv_right : EF x y · fully_faithful_precomp_inv = identity _.
proof: Proof. unfold fully_faithful_precomp_inv. rewrite !assoc. refine (_ @ z_iso_inv_after_z_iso φ). apply maponpaths_2. apply idpath. 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.Monoidal.Categories