Definition adjunction_from_adjunction_univ_cats {C₁ C₂ : bicat_of_univ_cats} : Bicategories.Morphisms.Adjunctions.adjunction C₁ C₂ → CategoryTheory.Adjunctions.Core.adjunction (pr1 C₁) (pr1 C₂). Proof. intros L. simple refine ((_ ,, (_ ,, (_ ,, _))) ,, (_ ,, _)). - exact (arrow_of_adjunction L). - exact (internal_right_adjoint L). - exact (left_adjoint_unit (left_adjoint_of_adjunction L)). - exact (left_adjoint_counit (left_adjoint_of_adjunction L)). - abstract (intro x ; cbn ; pose (nat_trans_eq_pointwise (pr122 L) x) as p ; cbn in p ; rewrite !id_left, !id_right in p ; exact p). - abstract (intro x ; cbn ; pose (nat_trans_eq_pointwise (pr222 L) x) as p ; cbn in p ; rewrite !id_left, !id_right in p ; exact p). Defined.
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.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.Core.Examples.OpMorBicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. Require Import UniMath.Bicategories.Morphisms.Examples.MorphismsInOp1Bicat.