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