proposition: Proposition fully_faithful_enriched_nat_z_iso_inv_right : EG x y · fully_faithful_enriched_nat_z_iso_inv = identity _.
proof: Proof. cbn. refine (_ @ z_iso_inv_after_z_iso φ). rewrite !assoc. apply maponpaths_2. rewrite (nat_trans_enrichment_to_comp Hα x y). rewrite !assoc'. rewrite <- postcomp_arr_comp. etrans. { do 2 apply maponpaths. exact (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso α y)). } rewrite postcomp_arr_id. apply id_right. 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