proposition: Lemma disp_left_adjoint_axioms_ptdfunctor_in_moncat : disp_left_adjoint_axioms adj_equivalence_ptdfunctor_in_cat disp_left_adjoint_data_ptdfunctor_in_moncat.
proof: Proof. split. * use total2_paths_f. 2: { apply homset_property. } repeat (apply funextsec ; intro). apply homset_property. * use total2_paths_f. 2: { apply homset_property. } repeat (apply funextsec ; intro). apply homset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors UniMath.CategoryTheory.Monoidal.Displayed.Monoidal UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.CategoryTheory.coslicecat UniMath.Bicategories.Core.Bicat UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects UniMath.Bicategories.MonoidalCategories.PointedFunctorsWhiskeredMonoidal UniMath.Bicategories.MonoidalCategories.EndofunctorsWhiskeredMonoidal UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Examples.BicatOfCats UniMath.Bicategories.MonoidalCategories.BicatOfWhiskeredMonCats UniMath.Bicategories.DisplayedBicats.DispAdjunctions