fact: Definition fully_faithful_enriched_nat_z_iso_inv : E₂ ⦃ G x , G y ⦄ --> E₁ ⦃ x, y ⦄ := precomp_arr _ _ (α x) · postcomp_arr _ _ (inv_from_z_iso (nat_z_iso_pointwise_z_iso α y)) · inv_from_z_iso φ.
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