Definition pb_of_sopfib {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₂) : internal_sopfib p₁. Proof. apply internal_sfib_is_internal_sopfib. use (@pb_of_sfib (op2_bicat B) e₁ e₂ b₁ b₂ p₁ p₂ fe fb). - apply weq_op2_invertible_2cell. exact (inv_of_invertible_2cell γ). - apply to_op2_has_pb_ump. exact H. - apply internal_sopfib_is_internal_sfib. exact Hf. 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.