Definition psfunctor_preserves_adjequiv' {C D : bicat} (F : psfunctor C D) {a b : C} {f : a --> b} (Hf : left_adjoint_equivalence f) : left_adjoint_equivalence (#F f). Proof. use equiv_to_adjequiv. simple refine ((_ ,, (_ ,, _)) ,, (_ ,, _)). - exact (#F (left_adjoint_right_adjoint Hf)). - exact (psfunctor_id F _ • ##F (left_equivalence_unit_iso Hf) • (psfunctor_comp F _ _)^-1). - exact (psfunctor_comp F _ _ • ##F (left_adjoint_counit Hf) • (psfunctor_id F _)^-1). - cbn. is_iso. + apply psfunctor_id. + exact (psfunctor_is_iso F (left_equivalence_unit_iso Hf)). - cbn. is_iso. + apply psfunctor_comp. + exact (psfunctor_is_iso F (left_equivalence_counit_iso Hf)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. 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.