Definition pointwise_adjequiv {B₁ B₂ : bicat} {F₁ F₂ : psfunctor B₁ B₂} (σ : pstrans F₁ F₂) (Hf : left_adjoint_equivalence σ) : ∏ (X : B₁), left_adjoint_equivalence (σ X). Proof. intro X. pose (pr1 (left_adjoint_equivalence_total_disp_weq _ _ Hf)) as t₁. pose (pr1 (left_adjoint_equivalence_total_disp_weq _ _ t₁)) as t₂. pose (pr1 (left_adjoint_equivalence_total_disp_weq _ _ t₂)) as t₃. exact (is_adjequiv_to_all_is_adjequiv _ _ _ t₃ 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.BicategoryLaws. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map2Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Identitor. Require Import UniMath.Bicategories.PseudoFunctors.Display.Compositor. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations.