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 φ.
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.