Definition internal_sfib_is_internal_sopfib {B : bicat} {e b : B} {p : e --> b} (Hp : @internal_sfib (op2_bicat B) e b p) : internal_sopfib p. Proof. split. - intros x f g α. refine (internal_sfib_cleaving_lift_mor _ Hp α ,, internal_sfib_cleaving_lift_cell _ Hp α ,, weq_op2_invertible_2cell _ _ (internal_sfib_cleaving_com _ Hp α) ,, _ ,, internal_sfib_cleaving_over _ Hp α). apply is_cartesian_to_is_opcartesian_sfib. exact (internal_sfib_cleaving_is_cartesian _ Hp α). - intros x y h f g γ Hγ. apply is_cartesian_to_is_opcartesian_sfib. apply (pr2 Hp). apply is_opcartesian_to_is_cartesian_sfib. exact Hγ. 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.Core.Univalence. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration.