Proposition fully_faithful_enriched_nat_z_iso_inv_right : EG x y · fully_faithful_enriched_nat_z_iso_inv = identity _. 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.
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.