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). Proof. use total_bicat_has_pb. - apply disp_2cells_isaprop_subbicat. - intros. apply subbicat_disp_2cell_over. - use disp_locally_groupoid_subbicat. exact HB'. - exact HB. - apply (subbicat_disp_has_pb HB Hcone). + exact Hπ₁. + exact Hπ₂. + exact H_ump_mor. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.EilenbergMooreObjects. Require Import UniMath.Bicategories.Limits.Examples.TotalBicategoryLimits. Require Import UniMath.Bicategories.Monads.Examples.MonadsInTotalBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion.