fact: Definition subbicat_has_pb (HB : has_pb B) (HB' : is_univalent_2 B) (Hcone : ∏ (x y z : subbicat P₀ P₁ Pid Pcomp) (f : x --> z) (g : y --> z), P₀ (pr1 (HB _ _ _ (pr1 f) (pr1 g)))) (Hπ₁ : ∏ (x y z : subbicat P₀ P₁ Pid Pcomp) (f : x --> z) (g : y --> z), P₁ _ _ (Hcone x y z f g) (pr12 x) (pb_cone_pr1 (pr1 (HB _ _ _ (pr1 f) (pr1 g))))) (Hπ₂ : ∏ (x y z : subbicat P₀ P₁ Pid Pcomp) (f : x --> z) (g : y --> z), P₁ _ _ (Hcone x y z f g) (pr12 y) (pb_cone_pr2 (pr1 (HB _ _ _ (pr1 f) (pr1 g))))) (H_ump_mor : ∏ (x y z : subbicat P₀ P₁ Pid Pcomp) (f : x --> z) (g : y --> z) (q : pb_cone f g), P₁ _ _ (pr121 q) (Hcone x y z f g) (pb_ump_mor (pr2 (HB (pr1 x) (pr1 y) (pr1 z) (pr1 f) (pr1 g))) (total_pb_cone_help_cone _ q))) : has_pb (subbicat P₀ P₁ Pid Pcomp).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.DisplayedCats.Core UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Univalence UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax UniMath.Bicategories.Limits.Final UniMath.Bicategories.Limits.Products UniMath.Bicategories.Limits.Pullbacks UniMath.Bicategories.Limits.EilenbergMooreObjects UniMath.Bicategories.Limits.Examples.TotalBicategoryLimits UniMath.Bicategories.Monads.Examples.MonadsInTotalBicat UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion