fact: Definition adj_equiv_to_pb_ump_2_cell : φ ==> ψ.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Morphisms.FullyFaithful UniMath.Bicategories.Morphisms.Properties UniMath.Bicategories.Morphisms.Properties.Projections UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispPseudofunctor UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.CleavingOfBicat UniMath.Bicategories.DisplayedBicats.CartesianPseudoFunctor UniMath.Bicategories.DisplayedBicats.Examples.Trivial UniMath.Bicategories.DisplayedBicats.Examples.Codomain UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.TrivialCleaving UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.CodomainCleaving UniMath.Bicategories.Limits.Products UniMath.Bicategories.Limits.Pullbacks UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.Identity UniMath.Bicategories.Logic.ComprehensionBicat