Definition internal_sopfib_is_internal_sfib {B : bicat} {e b : B} {p : e --> b} (Hp : internal_sopfib p) : @internal_sfib (op2_bicat B) e b p. Proof. split. - intros x f g α. refine (internal_sopfib_opcleaving_lift_mor _ Hp α ,, internal_sopfib_opcleaving_lift_cell _ Hp α ,, weq_op2_invertible_2cell _ _ (internal_sopfib_opcleaving_com _ Hp α) ,, _ ,, internal_sopfib_opcleaving_over _ Hp α). apply is_opcartesian_to_is_cartesian_sfib. exact (internal_sopfib_opcleaving_is_opcartesian _ Hp α). - intros x y h f g γ Hγ. apply is_opcartesian_to_is_cartesian_sfib. apply (pr2 Hp). apply is_cartesian_to_is_opcartesian_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.