Definition pb_of_sfib_cleaving : internal_sfib_cleaving p₁ := λ x h₁ h₂ α, pb_of_sfib_cleaving_mor α ,, pb_of_sfib_cleaving_cell α ,, pb_of_sfib_cleaving_over α ,, pb_of_sfib_cleaving_cell_is_cartesian_2cell_sfib α ,, pb_of_sfib_cleaving_commute α. Section FromPBCartesian. Context {x : B} {g₁ g₂ : x --> e₁} (α : g₁ ==> g₂) (Hα : is_cartesian_2cell_sfib p₁ α). Let g₀ : x --> e₁ := pb_of_sfib_cleaving_mor (α ▹ p₁). Let β : g₀ ==> g₂ := pb_of_sfib_cleaving_cell (α ▹ p₁). Let Hβ : is_cartesian_2cell_sfib p₁ β. Proof. apply pb_of_sfib_cleaving_cell_is_cartesian_2cell_sfib. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Require Import UniMath.Bicategories.Morphisms.Properties.Composition. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.Examples.OpCellBicatLimits. Section FromPBCartesian. End FromPBCartesian.