Definition mor_preserves_opcartesian_pb_ump_mor_comp {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) (Hf : internal_sopfib p₂) {c : B} {cp : c --> e₂} {h : c --> b₁} (δ : invertible_2cell (cp · p₂) (h · fb)) (cone := make_pb_cone c cp h δ : pb_cone p₂ fb) (Hfmap : mor_preserves_opcartesian (cp · p₂) p₂ cp) (Hgmap : mor_preserves_opcartesian (cp · p₂) fb h) : mor_preserves_opcartesian (cp · p₂) (fe · p₂) (pb_ump_mor H cone). Proof. apply mor_preserves_cartesian_to_mor_preserves_opcartesian. exact (@mor_preserves_cartesian_pb_ump_mor_comp (op2_bicat B) e₁ e₂ b₁ b₂ p₁ p₂ fe fb _ (to_op2_has_pb_ump _ H) (internal_sopfib_is_internal_sfib Hf) c cp h (inv_of_invertible_2cell (weq_op2_invertible_2cell _ _ δ)) (mor_preserves_opcartesian_to_mor_preserves_cartesian Hfmap) (mor_preserves_opcartesian_to_mor_preserves_cartesian Hgmap)). 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.