Definition left_adjoint_to_is_left_adjoint {C₁ C₂ : bicat_of_univ_cats} {L : C₁ --> C₂} (HL : left_adjoint L) : is_left_adjoint L. Proof. simple refine (left_adjoint_right_adjoint HL ,, ((left_adjoint_unit HL ,, left_adjoint_counit HL) ,, _)). split. - abstract (intro x ; cbn ; pose (nat_trans_eq_pointwise (internal_triangle1 HL) x) as p ; cbn in p ; rewrite !id_left, !id_right in p ; exact p). - abstract (intro x ; cbn ; pose (nat_trans_eq_pointwise (internal_triangle2 HL) 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.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.