proposition: Lemma disp_left_universal_arrow_is_functor {x : B2} (xx : D2 x) {y : B1} (yy : D1 y) : disp_functor_axioms (disp_left_universal_arrow_functor_data xx yy).
proof: Proof. set (lur := left_universal_arrow_functor (total_psfunctor _ _ _ RR) (x,,xx) (y,,yy) η0). split. - intros f ff. set (p := pr12 lur (f,,ff)). refine (fiber_paths_transposed _ _ p @ _). apply maponpaths_2. apply cellset_property. - intros f g h ff gg hh α β αα ββ. set (p := pr22 lur (f,,ff) (g,,gg) (h,,hh) (α,,αα) (β,,ββ)). set (s := fiber_paths_transposed _ _ p). refine (s @ _). apply maponpaths_2. apply cellset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.CompositesAndInverses UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.FullyFaithful UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Adjunctions UniMath.CategoryTheory.DisplayedCats.Equivalences UniMath.CategoryTheory.DisplayedCats.TotalAdjunction UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Univalence UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispPseudofunctor UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.Transformations.PseudoTransformation UniMath.Bicategories.PseudoFunctors.Biadjunction UniMath.Bicategories.Modifications.Modification UniMath.Bicategories.PseudoFunctors.UniversalArrow UniMath.Bicategories.DisplayedBicats.DispBiadjunction UniMath.Bicategories.DisplayedBicats.DispInvertibles