Definition all_is_adjequiv_to_is_adjequiv {F G : ps_base} (η : F --> G) : (∏ (X : C), left_adjoint_equivalence (η X)) → left_adjoint_equivalence η. Proof. intros Hη. use tpair. - use tpair. + intros X. exact (pr11 (Hη X)). + split ; intros X ; cbn. * exact (pr121 (Hη X)). * exact (pr221 (Hη X)). - split ; split ; cbn. + apply funextsec ; intro X. exact (pr112 (Hη X)). + apply funextsec ; intro X. exact (pr212 (Hη X)). + apply all_is_invertible_is_is_invertible_2cell. exact (λ X, pr122 (Hη X)). + apply all_is_invertible_is_is_invertible_2cell. exact (λ X, pr222 (Hη X)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. 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.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique.