Definition to_pb_cartesian {x : B} {g₁ g₂ : x --> e₁} (α : g₁ ==> g₂) (Hα : is_cartesian_2cell_sfib p₂ (α ▹ fe)) : is_cartesian_2cell_sfib p₁ α. Proof. intros h β δp q. use iscontraprop1. - exact (to_pb_cartesian_unique α Hα q). - simple refine (_ ,, _ ,, _). + exact (to_pb_cartesian_cell α Hα q). + apply (pb_ump_cell_pr2 H). + exact (to_pb_cartesian_comm α Hα q). 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.