Proposition adjunction_enrichment_hom_is_inverse (x : C₁) (y : C₂) : is_inverse_in_precat (adjunction_enrichment_left_hom x y) (adjunction_enrichment_right_hom x y). Proof. split ; unfold adjunction_enrichment_left_hom, adjunction_enrichment_right_hom. - rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite <- functor_enrichment_precomp_arr. rewrite !assoc'. apply maponpaths. apply idpath. } rewrite precomp_postcomp_arr. rewrite !assoc. etrans. { apply maponpaths_2. exact (!(nat_trans_enrichment_to_comp Eε (L x) y)). } cbn. rewrite id_left. rewrite <- precomp_arr_comp. refine (_ @ precomp_arr_id _ _ _). apply maponpaths. exact (triangle_1_statement_from_adjunction A x). - rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite <- functor_enrichment_postcomp_arr. rewrite !assoc'. apply maponpaths. apply idpath. } rewrite <- precomp_postcomp_arr. rewrite !assoc. etrans. { apply maponpaths_2. exact (nat_trans_enrichment_to_comp Eη x (R y)). } cbn. rewrite id_left. rewrite <- postcomp_arr_comp. refine (_ @ postcomp_arr_id _ _ _). apply maponpaths. exact (triangle_2_statement_from_adjunction A y). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.Monoidal.Categories.