Definition pointwise_adjequiv_to_adjequiv_data : left_adjoint_equivalence (pr1 σ). Proof. use (invmap (left_adjoint_equivalence_total_disp_weq _ _)). simple refine (_ ,, _). - exact pointwise_adjequiv_to_adjequiv_1cell. - use (pair_left_adjoint_equivalence (map2cells_disp_cat B₁ B₂) (disp_dirprod_bicat (identitor_disp_cat B₁ B₂) (compositor_disp_cat B₁ B₂)) (_ ,, pointwise_adjequiv_to_adjequiv_1cell)). simple refine (_ ,, _). + apply map2cells_disp_left_adjequiv. exact HB₂. + use (pair_left_adjoint_equivalence (identitor_disp_cat B₁ B₂) (compositor_disp_cat B₁ B₂)). simple refine (_ ,, _). * apply identitor_disp_left_adjequiv. exact HB₂. * apply compositor_disp_left_adjequiv. exact HB₂. 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.