Definition mor_preserves_opcartesian_pb_ump_mor_alt {B : bicat} {e₁ e₂ b₁ b₂ : B} {p₁ : e₁ --> b₁} {p₂ : e₂ --> b₂} {fe : e₁ --> e₂} {fb : b₁ --> b₂} {γ : invertible_2cell (fe · p₂) (p₁ · fb)} (pb := make_pb_cone e₁ fe p₁ γ) (H : has_pb_ump pb) {e₀ : B} (p₀ : e₀ --> b₁) (h₁ : e₀ --> e₂) (δ : invertible_2cell (h₁ · p₂) (p₀ · fb)) (cone := make_pb_cone e₀ h₁ p₀ δ) (Hh₁ : mor_preserves_opcartesian p₀ p₂ h₁) : mor_preserves_opcartesian p₀ p₁ (pb_ump_mor H cone). Proof. apply mor_preserves_cartesian_to_mor_preserves_opcartesian. exact (@mor_preserves_cartesian_pb_ump_mor_alt (op2_bicat B) e₁ e₂ b₁ b₂ p₁ p₂ fe fb _ (to_op2_has_pb_ump _ H) e₀ p₀ h₁ (inv_of_invertible_2cell (weq_op2_invertible_2cell _ _ δ)) (mor_preserves_opcartesian_to_mor_preserves_cartesian Hh₁)). 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.