Definition is_left_adjoint_to_left_adjoint {C₁ C₂ : bicat_of_univ_cats} {L : C₁ --> C₂} (HL : is_left_adjoint L) : left_adjoint L. Proof. simple refine ((right_functor HL ,, (adjunit HL ,, adjcounit HL)) ,, _). split. - abstract (use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; rewrite !id_left, !id_right ; apply (pr122 HL)). - abstract (use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; rewrite !id_left, !id_right ; apply (pr222 HL)). 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.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Univalence.