proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.Monoidal.Categories