fact: Definition fully_faithful_precomp_inv : E₂ ⦃ F x , F y ⦄ --> E₁ ⦃ x , y ⦄ := EG (F x) (F 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