Proposition fully_faithful_enriched_nat_z_iso_inv_left : fully_faithful_enriched_nat_z_iso_inv · EG x y = identity _. Proof. cbn. refine (_ @ postcomp_arr_id _ _ _). refine (!_). etrans. { apply maponpaths. exact (!(z_iso_after_z_iso_inv (nat_z_iso_pointwise_z_iso α y))). } cbn. rewrite precomp_postcomp_arr. rewrite postcomp_arr_comp. rewrite !assoc'. apply maponpaths. refine (!(id_left _) @ _). rewrite <- precomp_arr_id. etrans. { apply maponpaths_2. apply maponpaths. exact (!(z_iso_after_z_iso_inv (nat_z_iso_pointwise_z_iso α x))). } rewrite precomp_arr_comp. rewrite !assoc'. apply maponpaths. rewrite precomp_postcomp_arr. etrans. { apply maponpaths_2. refine (!(id_left _) @ _). rewrite <- (z_iso_after_z_iso_inv φ). rewrite !assoc'. apply maponpaths. exact (!(nat_trans_enrichment_to_comp Hα x y)). } rewrite !assoc'. rewrite <- precomp_arr_comp. etrans. { do 3 apply maponpaths. exact (z_iso_after_z_iso_inv (nat_z_iso_pointwise_z_iso α x)). } rewrite precomp_arr_id. rewrite id_right. apply idpath. 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.