Definition is_adjequiv_to_all_is_adjequiv {F G : ps_base} (η : F --> G) : left_adjoint_equivalence η → (∏ (X : C), left_adjoint_equivalence (η X)). Proof. intros Hη X. use tpair. - use tpair. + exact (pr11 Hη X). + split ; cbn. * exact (pr121 Hη X). * exact (pr221 Hη X). - split ; split ; cbn. + exact (maponpaths (λ φ, φ X) (pr112 Hη)). + exact (maponpaths (λ φ, φ X) (pr212 Hη)). + exact (is_invertible_2cell_to_all_is_invertible (pr121 Hη) (pr122 Hη) X). + exact (is_invertible_2cell_to_all_is_invertible (pr221 Hη) (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.