Library UniMath.Bicategories.Morphisms.Examples.FibrationsInBicatOfUnivCats

Fibrations in the bicat of univalent categories
Contents: 1. Internal Street Fibrations 2. Internal Street Opfibrations
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.categories.StandardCategories.
Require Import UniMath.CategoryTheory.DisplayedCats.StreetFibration.
Require Import UniMath.CategoryTheory.DisplayedCats.StreetOpFibration.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration.
Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration.

Local Open Scope cat.

1. Internal Street Fibrations
Section InternalSFibToStreetFib.
  Context {C₁ C₂ : bicat_of_univ_cats}
          {F : C₁ --> C₂}
          (HF : internal_sfib F).

  Section InternalSFibToStreetFibFactor.
    Context {G₁ G₂ : (unit_category : bicat_of_univ_cats) --> C₁}
            {α : G₁ ==> G₂}
            (Hα : is_cartesian_2cell_sfib F α)
            {z : pr1 C₁}
            {g : z --> pr1 G₂ tt}
            {h : pr1 F z --> pr1 F (pr1 G₁ tt)}
            (q : # (pr1 F) g = h · # (pr1 F) (pr1 α tt)).

    Let Φ : unit_category ⟶ pr1 C₁
      := functor_from_unit z.

    Local Definition internal_sfib_is_cartesian_sfib_factor_nat_trans_1
      : Φ ⟹ pr1 G₂.
    Show proof.
      use make_nat_trans.
      - intro x ; induction x.
        exact g.
      - abstract
          (intros x y f ; cbn ;
           induction x ; induction y ;
           cbn ;
           assert (p : f = identity _) ; [ apply isapropunit | ] ;
           rewrite p ;
           refine (id_left _ @ !(id_right _) @ _) ;
           apply maponpaths ;
           refine (!_) ;
           apply functor_id).

    Let ζ := internal_sfib_is_cartesian_sfib_factor_nat_trans_1.

    Local Definition internal_sfib_is_cartesian_sfib_factor_nat_trans_2
      : Φ ∙ F ⟹ G₁ ∙ F.
    Show proof.
      use make_nat_trans.
      - intros x ; induction x.
        exact h.
      - abstract
          (intros x y f ; cbn ;
           induction x ; induction y ;
           cbn ;
           assert (p : f = identity _) ; [ apply isapropunit | ] ;
           rewrite p ;
           rewrite (functor_id G₁) ;
           rewrite !(functor_id F) ;
           rewrite id_left, id_right ;
           apply idpath).

    Let ξ := internal_sfib_is_cartesian_sfib_factor_nat_trans_2.

    Local Lemma internal_sfib_is_cartesian_sfib_factor_eq
      : post_whisker ζ F
        =
        nat_trans_comp _ _ _ ξ (post_whisker α F).
    Show proof.
      use nat_trans_eq.
      {
        apply homset_property.
      }
      intro x ; induction x.
      exact q.

    Let p := internal_sfib_is_cartesian_sfib_factor_eq.

    Definition internal_sfib_is_cartesian_sfib_factor
      : z --> pr1 G₁ tt
      := pr1 (is_cartesian_2cell_sfib_factor _ Hα ζ ξ p) tt.

    Definition internal_sfib_is_cartesian_sfib_factor_over
      : # (pr1 F) internal_sfib_is_cartesian_sfib_factor = h.
    Show proof.
      exact (nat_trans_eq_pointwise
              (is_cartesian_2cell_sfib_factor_over _ Hα p)
              tt).

    Definition internal_sfib_is_cartesian_sfib_factor_comm
      : internal_sfib_is_cartesian_sfib_factor · pr1 α tt = g.
    Show proof.
      exact (nat_trans_eq_pointwise
               (is_cartesian_2cell_sfib_factor_comm _ Hα p)
               tt).

    Local Definition internal_sfib_is_cartesian_sfib_factor_unique_help
               (k : z --> pr1 G₁ tt)
      : Φ ⟹ pr1 G₁.
    Show proof.
      use make_nat_trans.
      - intro x ; induction x.
        exact k.
      - abstract
          (intros x y f ;
           induction x ; induction y ; cbn ;
           assert (r : f = identity _) ; [ apply isapropunit | ] ;
           rewrite r ;
           rewrite !(functor_id G₁) ;
           rewrite id_left, id_right ;
           apply idpath).

    Definition internal_sfib_is_cartesian_sfib_factor_unique
      : isaprop (∑ φ, # (pr1 F) φ = h × φ · pr1 α tt = g).
    Show proof.
      use invproofirrelevance.
      intros φ₁ φ₂.
      use subtypePath.
      {
        intro.
        apply isapropdirprod ; apply homset_property.
      }
      refine (nat_trans_eq_pointwise
                (is_cartesian_2cell_sfib_factor_unique
                   _ Hα
                   Φ ζ ξ p
                   (internal_sfib_is_cartesian_sfib_factor_unique_help (pr1 φ₁))
                   (internal_sfib_is_cartesian_sfib_factor_unique_help (pr1 φ₂))
                   _ _ _ _)
                tt) ;
        (use nat_trans_eq ; [ apply homset_property | ]) ;
        intro x ; induction x ; cbn.
      - exact (pr12 φ₁).
      - exact (pr12 φ₂).
      - exact (pr22 φ₁).
      - exact (pr22 φ₂).
  End InternalSFibToStreetFibFactor.

  Definition internal_sfib_is_cartesian_sfib
             {G₁ G₂ : (unit_category : bicat_of_univ_cats) --> C₁}
             {α : G₁ ==> G₂}
             (Hα : is_cartesian_2cell_sfib F α)
    : is_cartesian_sfib F (pr1 α tt).
  Show proof.
    intros z g h q.
    use iscontraprop1.
    - exact (internal_sfib_is_cartesian_sfib_factor_unique Hα q).
    - simple refine (_ ,, _ ,, _).
      + exact (internal_sfib_is_cartesian_sfib_factor Hα q).
      + exact (internal_sfib_is_cartesian_sfib_factor_over Hα q).
      + exact (internal_sfib_is_cartesian_sfib_factor_comm Hα q).

  Section Cleaving.
    Context {e : pr1 C₁}
            {b : pr1 C₂}
            (f : b --> pr1 F e).

    Definition internal_sfib_is_street_fib_nat_trans
      : functor_from_unit b ⟹ functor_from_unit e ∙ F.
    Show proof.
      use make_nat_trans.
      - exact (λ _, f).
      - abstract
          (intros z₁ z₂ g ; cbn ;
           rewrite id_left, functor_id, id_right ;
           apply idpath).

    Let ℓ := pr1 HF _ _ _ internal_sfib_is_street_fib_nat_trans.

    Definition internal_sfib_is_street_fib_lift_ob
      : pr1 C₁
      := pr1 (pr1 ℓ) tt.

    Definition internal_sfib_is_street_fib_lift_mor
      : internal_sfib_is_street_fib_lift_ob --> e
      := pr1 (pr12 ℓ) tt.

    Definition internal_sfib_is_street_fib_lift_z_iso
      : z_iso (pr1 F internal_sfib_is_street_fib_lift_ob) b
      := nat_z_iso_pointwise_z_iso (invertible_2cell_to_nat_z_iso _ _ (pr122 ℓ)) tt.

    Definition internal_sfib_is_street_fib_lift_over
      : # (pr1 F) internal_sfib_is_street_fib_lift_mor
        =
        internal_sfib_is_street_fib_lift_z_iso · f
      := nat_trans_eq_pointwise (pr2 (pr222 ℓ)) tt.

    Definition internal_sfib_is_street_fib_lift_cartesian
      : is_cartesian_sfib F internal_sfib_is_street_fib_lift_mor
      := internal_sfib_is_cartesian_sfib (pr1 (pr222 ℓ)).
  End Cleaving.

  Definition internal_sfib_is_street_fib
    : street_fib F.
  Show proof.
    intros e b f.
    simple refine (_ ,, (_ ,, _) ,, _ ,, _) ; cbn.
    - exact (internal_sfib_is_street_fib_lift_ob f).
    - exact (internal_sfib_is_street_fib_lift_mor f).
    - exact (internal_sfib_is_street_fib_lift_z_iso f).
    - exact (internal_sfib_is_street_fib_lift_over f).
    - exact (internal_sfib_is_street_fib_lift_cartesian f).
End InternalSFibToStreetFib.

Section StreetFibToInternalSFib.
  Context {C₁ C₂ : bicat_of_univ_cats}
          {F : C₁ --> C₂}
          (HF : street_fib F).

  Section IsCartesian.
    Context {C₀ : bicat_of_univ_cats}
            {G₁ G₂ : C₀ --> C₁}
            (α : G₁ ==> G₂)
            (Hα : ∏ (x : pr1 C₀), is_cartesian_sfib F (pr1 α x)).

    Section Factorization.
      Context {H : C₀ --> C₁}
              {β : H ==> G₂}
              {δp : H · F ==> G₁ · F}
              (q : β ▹ F = δp • (α ▹ F)).

      Definition pointwise_cartesian_is_cartesian_factor_data
        : nat_trans_data (pr1 H) (pr1 G₁)
        := λ x,
           cartesian_factorization_sfib
             _
             (Hα x)
             (pr1 β x)
             (pr1 δp x)
             (nat_trans_eq_pointwise q x).

      Definition pointwise_cartesian_is_cartesian_factor_laws
        : is_nat_trans _ _ pointwise_cartesian_is_cartesian_factor_data.
      Show proof.
        intros x y f ; unfold pointwise_cartesian_is_cartesian_factor_data ; cbn.
        pose (cartesian_factorization_sfib_commute
                F
                (Hα x) (pr1 β x) (pr1 δp x)
                (nat_trans_eq_pointwise q x))
          as p.
        pose (cartesian_factorization_sfib_commute
                F
                (Hα y) (pr1 β y) (pr1 δp y)
                (nat_trans_eq_pointwise q y))
          as p'.
        use (cartesian_factorization_sfib_unique
               _
               (Hα y)
               (pr1 β x · # (pr1 G₂) f)
               (pr1 δp x · # (pr1 F) (# (pr1 G₁) f))).
        - rewrite functor_comp.
          pose (r := nat_trans_eq_pointwise q x) ; cbn in r.
          etrans.
          {
            apply maponpaths_2.
            exact r.
          }
          clear r.
          rewrite !assoc'.
          apply maponpaths.
          refine (!(functor_comp _ _ _) @ _ @ functor_comp _ _ _).
          apply maponpaths.
          exact (!(nat_trans_ax α _ _ f)).
        - rewrite functor_comp.
          rewrite cartesian_factorization_sfib_over.
          exact (nat_trans_ax δp _ _ f).
        - rewrite !functor_comp.
          rewrite cartesian_factorization_sfib_over.
          apply idpath.
        - rewrite !assoc'.
          etrans.
          {
            apply maponpaths.
            exact p'.
          }
          exact (nat_trans_ax β _ _ f).
        - rewrite !assoc'.
          etrans.
          {
            apply maponpaths.
            exact (nat_trans_ax α _ _ f).
          }
          rewrite assoc.
          apply maponpaths_2.
          exact p.

      Definition pointwise_cartesian_is_cartesian_factor
        : H ==> G₁.
      Show proof.
        use make_nat_trans.
        - exact pointwise_cartesian_is_cartesian_factor_data.
        - exact pointwise_cartesian_is_cartesian_factor_laws.

      Definition pointwise_cartesian_is_cartesian_over
        : pointwise_cartesian_is_cartesian_factor ▹ F = δp.
      Show proof.
        use nat_trans_eq.
        {
          apply homset_property.
        }
        intro x ; cbn.
        apply cartesian_factorization_sfib_over.

      Definition pointwise_cartesian_is_cartesian_comm
        : pointwise_cartesian_is_cartesian_factor • α = β.
      Show proof.
        use nat_trans_eq.
        {
          apply homset_property.
        }
        intro x ; cbn.
        apply cartesian_factorization_sfib_commute.

      Definition pointwise_cartesian_is_cartesian_unique
        : isaprop (∑ (δ : H ==> G₁), δ ▹ F = δp × δ • α = β).
      Show proof.
        use invproofirrelevance.
        intros δ₁ δ₂.
        use subtypePath.
        {
          intro.
          apply isapropdirprod ; apply cellset_property.
        }
        use nat_trans_eq.
        {
          apply homset_property.
        }
        intro x.
        use (cartesian_factorization_sfib_unique
               _ (Hα x)
               (pr1 β x)
               (pr1 δp x)).
        - exact (nat_trans_eq_pointwise q x).
        - exact (nat_trans_eq_pointwise (pr12 δ₁) x).
        - exact (nat_trans_eq_pointwise (pr12 δ₂) x).
        - exact (nat_trans_eq_pointwise (pr22 δ₁) x).
        - exact (nat_trans_eq_pointwise (pr22 δ₂) x).
    End Factorization.

    Definition pointwise_cartesian_is_cartesian
      : is_cartesian_2cell_sfib F α.
    Show proof.
      intros H β δp q.
      use iscontraprop1.
      - exact (pointwise_cartesian_is_cartesian_unique q).
      - simple refine (_ ,, _ ,, _).
        + exact (pointwise_cartesian_is_cartesian_factor q).
        + exact (pointwise_cartesian_is_cartesian_over q).
        + exact (pointwise_cartesian_is_cartesian_comm q).
  End IsCartesian.

  Section Cleaving.
    Context {C₀ : bicat_of_univ_cats}
            {G₁ : C₀ --> C₂}
            {G₂ : C₀ --> C₁}
            (α : G₁ ==> G₂ · F).

    Definition street_fib_is_internal_sfib_cleaving_lift_data
      : functor_data (pr1 C₀) (pr1 C₁).
    Show proof.
      use make_functor_data.
      - exact (λ x, pr1 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x))).
      - intros x y f ; cbn.
        use (cartesian_factorization_sfib
               _
               (pr222 (HF (pr1 G₂ y) (pr1 G₁ y) (pr1 α y)))).
        + exact (pr112 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)) · # (pr1 G₂) f).
        + exact (pr212 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x))
                 · # (pr1 G₁) f
                 · inv_from_z_iso (pr212 (HF (pr1 G₂ y) (pr1 G₁ y) (pr1 α y)))).
        + abstract
            (rewrite functor_comp ;
             rewrite (pr122 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x))) ;
             rewrite !assoc' ;
             apply maponpaths ;
             refine (!(nat_trans_ax α _ _ f) @ _) ;
             apply maponpaths ;
             refine (!_) ;
             use z_iso_inv_on_right ;
             rewrite (pr122 (HF (pr1 G₂ y) (pr1 G₁ y) (pr1 α y))) ;
             apply idpath).

    Definition street_fib_is_internal_sfib_cleaving_lift_is_functor
      : is_functor street_fib_is_internal_sfib_cleaving_lift_data.
    Show proof.
      split.
      - intro x ; cbn.
        use (cartesian_factorization_sfib_unique
               _
               (pr222 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)))).
        + exact (pr112 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x))).
        + apply identity.
        + rewrite id_left.
          apply idpath.
        + rewrite cartesian_factorization_sfib_over.
          refine (!_).
          use z_iso_inv_on_left.
          rewrite id_left.
          rewrite (functor_id G₁).
          rewrite id_right.
          apply idpath.
        + apply functor_id.
        + rewrite cartesian_factorization_sfib_commute.
          rewrite (functor_id G₂).
          apply id_right.
        + apply id_left.
      - intros x y z f g ; cbn.
        use (cartesian_factorization_sfib_unique
               _
               (pr222 (HF (pr1 G₂ z) (pr1 G₁ z) (pr1 α z)))).
        + exact (pr112 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)) · # (pr1 G₂) (f · g)).
        + exact (pr212 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x))
                 · # (pr1 G₁) (f · g)
                 · inv_from_z_iso (pr212 (HF (pr1 G₂ z) (pr1 G₁ z) (pr1 α z)))).
        + rewrite functor_comp.
          etrans.
          {
            apply maponpaths_2.
            exact (pr122 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x))).
          }
          rewrite !assoc'.
          apply maponpaths.
          refine (!(nat_trans_ax α _ _ (f · g)) @ _).
          apply maponpaths.
          refine (!_).
          use z_iso_inv_on_right.
          exact (pr122 (HF (pr1 G₂ z) (pr1 G₁ z) (pr1 α z))).
        + apply cartesian_factorization_sfib_over.
        + rewrite functor_comp.
          rewrite !cartesian_factorization_sfib_over.
          rewrite !assoc'.
          apply maponpaths.
          rewrite !assoc.
          apply maponpaths_2.
          rewrite (functor_comp G₁).
          rewrite !assoc'.
          apply maponpaths.
          rewrite !assoc.
          rewrite z_iso_after_z_iso_inv.
          apply id_left.
        + apply cartesian_factorization_sfib_commute.
        + rewrite !assoc'.
          rewrite cartesian_factorization_sfib_commute.
          rewrite !assoc.
          rewrite cartesian_factorization_sfib_commute.
          rewrite !assoc'.
          rewrite (functor_comp G₂).
          apply idpath.

    Definition street_fib_is_internal_sfib_cleaving_lift
      : C₀ --> C₁.
    Show proof.
      use make_functor.
      - exact street_fib_is_internal_sfib_cleaving_lift_data.
      - exact street_fib_is_internal_sfib_cleaving_lift_is_functor.

    Definition street_fib_is_internal_sfib_cleaving_lift_mor_data
      : nat_trans_data
          street_fib_is_internal_sfib_cleaving_lift_data
          (pr1 G₂)
      := λ x, pr112 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)).

    Definition street_fib_is_internal_sfib_cleaving_lift_mor_is_nat_trans
      : is_nat_trans _ _ street_fib_is_internal_sfib_cleaving_lift_mor_data.
    Show proof.
      intros x y f ; cbn.
      apply cartesian_factorization_sfib_commute.

    Definition street_fib_is_internal_sfib_cleaving_lift_mor
      : street_fib_is_internal_sfib_cleaving_lift ==> G₂.
    Show proof.
      use make_nat_trans.
      - exact street_fib_is_internal_sfib_cleaving_lift_mor_data.
      - exact street_fib_is_internal_sfib_cleaving_lift_mor_is_nat_trans.

    Definition street_fib_is_internal_sfib_cleaving_lift_over_nat_trans_data
      : nat_trans_data (street_fib_is_internal_sfib_cleaving_lift ∙ F) (pr1 G₁)
      := λ x, pr212 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)).

    Definition street_fib_is_internal_sfib_cleaving_lift_over_is_nat_trans
      : is_nat_trans
          _ _
          street_fib_is_internal_sfib_cleaving_lift_over_nat_trans_data.
    Show proof.
      intros x y f ; cbn.
      unfold street_fib_is_internal_sfib_cleaving_lift_over_nat_trans_data.
      rewrite cartesian_factorization_sfib_over.
      rewrite !assoc'.
      rewrite z_iso_after_z_iso_inv.
      rewrite id_right.
      apply idpath.

    Definition street_fib_is_internal_sfib_cleaving_lift_over_nat_trans
      : street_fib_is_internal_sfib_cleaving_lift ∙ F ⟹ pr1 G₁.
    Show proof.
      use make_nat_trans.
      - exact street_fib_is_internal_sfib_cleaving_lift_over_nat_trans_data.
      - exact street_fib_is_internal_sfib_cleaving_lift_over_is_nat_trans.

    Definition street_fib_is_internal_sfib_cleaving_lift_cartesian
      : is_cartesian_2cell_sfib
          F
          street_fib_is_internal_sfib_cleaving_lift_mor.
    Show proof.
      use pointwise_cartesian_is_cartesian.
      intro x.
      exact (pr222 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x))).

    Definition street_fib_is_internal_sfib_cleaving_lift_over
      : invertible_2cell
          (street_fib_is_internal_sfib_cleaving_lift · F)
          G₁.
    Show proof.
      use nat_z_iso_to_invertible_2cell.
      use make_nat_z_iso.
      - exact street_fib_is_internal_sfib_cleaving_lift_over_nat_trans.
      - intro x.
        apply z_iso_is_z_isomorphism.
  End Cleaving.

  Definition street_fib_is_internal_sfib_cleaving
    : internal_sfib_cleaving F.
  Show proof.
    intros C₀ G₁ G₂ α.
    simple refine (_ ,, _ ,, _ ,, _ ,, _).
    - exact (street_fib_is_internal_sfib_cleaving_lift α).
    - exact (street_fib_is_internal_sfib_cleaving_lift_mor α).
    - exact (street_fib_is_internal_sfib_cleaving_lift_over α).
    - exact (street_fib_is_internal_sfib_cleaving_lift_cartesian α).
    - abstract
        (use nat_trans_eq ; [ apply homset_property | ] ;
         intro x ; cbn ;
         exact (pr122 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)))).

  Section IsCartesian.
    Context {C₀ : bicat_of_univ_cats}
            {G₁ G₂ : C₀ --> C₁}
            (α : G₁ ==> G₂)
            (Hα : is_cartesian_2cell_sfib F α).

    Definition pointwise_lift_functor_data
      : functor_data (pr1 C₀) (pr1 C₁).
    Show proof.
      use make_functor_data.
      - exact (λ x, pr1 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))).
      - intros x y f ; cbn.
        use (cartesian_factorization_sfib
               _
               (pr222 (HF (pr1 G₂ y) (pr1 F (pr1 G₁ y)) (# (pr1 F) (pr1 α y))))).
        + exact (pr112 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))
                 · # (pr1 G₂) f).
        + exact (pr212 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))
                 · # (pr1 F) (# (pr1 G₁) f)
                 · inv_from_z_iso
                     (pr212 (HF (pr1 G₂ y) (pr1 F (pr1 G₁ y)) (# (pr1 F) (pr1 α y))))).
        + abstract
            (rewrite functor_comp ;
             rewrite (pr122 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))) ;
             rewrite !assoc' ;
             apply maponpaths ;
             rewrite <- (functor_comp F) ;
             etrans ;
             [ apply maponpaths ;
               exact (!(nat_trans_ax α _ _ f))
             | ] ;
             rewrite functor_comp ;
             apply maponpaths ;
             refine (!_) ;
             use z_iso_inv_on_right ;
             rewrite (pr122 (HF (pr1 G₂ y) (pr1 F (pr1 G₁ y)) (# (pr1 F) (pr1 α y)))) ;
             apply idpath).

    Definition pointwise_lift_functor_is_functor
      : is_functor pointwise_lift_functor_data.
    Show proof.
      split.
      - intro x ; cbn.
        use (cartesian_factorization_sfib_unique
               _
               (pr222 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x))))).
        + exact (pr112 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))).
        + apply identity.
        + rewrite id_left.
          apply idpath.
        + rewrite cartesian_factorization_sfib_over.
          refine (!_).
          use z_iso_inv_on_left.
          rewrite id_left.
          rewrite (functor_id G₁).
          rewrite (functor_id F).
          apply id_right.
        + apply functor_id.
        + rewrite cartesian_factorization_sfib_commute.
          rewrite (functor_id G₂).
          apply id_right.
        + apply id_left.
      - intros x y z f g ; cbn.
        use (cartesian_factorization_sfib_unique
               _
               (pr222 (HF (pr1 G₂ z) (pr1 F (pr1 G₁ z)) (# (pr1 F) (pr1 α z))))).
        + exact (pr112 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))
                 · # (pr1 G₂) (f · g)).
        + exact (pr212 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))
                 · # (pr1 F) (# (pr1 G₁) (f · g))
                 · inv_from_z_iso
                     (pr212 (HF (pr1 G₂ z) (pr1 F (pr1 G₁ z)) (# (pr1 F) (pr1 α z))))).
        + rewrite functor_comp.
          rewrite (pr122 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))).
          rewrite !assoc'.
          apply maponpaths.
          rewrite <- (functor_comp F).
          etrans.
          {
            apply maponpaths.
            exact (!(nat_trans_ax α _ _ (f · g))).
          }
          rewrite functor_comp.
          apply maponpaths.
          refine (!_).
          use z_iso_inv_on_right.
          rewrite (pr122 (HF (pr1 G₂ z) (pr1 F (pr1 G₁ z)) (# (pr1 F) (pr1 α z)))).
          apply idpath.
        + apply cartesian_factorization_sfib_over.
        + rewrite functor_comp.
          rewrite !cartesian_factorization_sfib_over.
          rewrite (functor_comp G₁).
          rewrite (functor_comp F).
          rewrite !assoc'.
          do 2 apply maponpaths.
          rewrite !assoc.
          apply maponpaths_2.
          rewrite !assoc'.
          use z_iso_inv_on_right.
          apply idpath.
        + apply cartesian_factorization_sfib_commute.
        + rewrite !assoc'.
          rewrite cartesian_factorization_sfib_commute.
          rewrite !assoc.
          rewrite cartesian_factorization_sfib_commute.
          rewrite !assoc'.
          rewrite (functor_comp G₂).
          apply idpath.

    Definition pointwise_lift_functor
      : C₀ --> C₁.
    Show proof.
      use make_functor.
      - exact pointwise_lift_functor_data.
      - exact pointwise_lift_functor_is_functor.

    Definition pointwise_lift_nat_trans_data
      : nat_trans_data pointwise_lift_functor_data (pr1 G₂)
      := λ x, pr112 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x))).

    Definition pointwise_lift_is_nat_trans
      : is_nat_trans _ _ pointwise_lift_nat_trans_data.
    Show proof.
      intros x y f ; cbn.
      unfold pointwise_lift_nat_trans_data.
      apply cartesian_factorization_sfib_commute.

    Definition pointwise_lift_nat_trans
      : pointwise_lift_functor ==> G₂.
    Show proof.
      use make_nat_trans.
      - exact pointwise_lift_nat_trans_data.
      - exact pointwise_lift_is_nat_trans.

    Definition pointwise_lift_nat_trans_is_cartesian_2cell
      : is_cartesian_2cell_sfib F pointwise_lift_nat_trans.
    Show proof.
      use pointwise_cartesian_is_cartesian.
      intro x.
      exact (pr222 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))).

    Definition is_cartesian_2cell_sfib_pointwise_cartesian_over_data
      : nat_trans_data (G₁ ∙ F) (pointwise_lift_functor ∙ F).
    Show proof.
      intro x.
      pose (i := pr212 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))).
      exact (z_iso_inv_from_z_iso i).

    Definition is_cartesian_2cell_sfib_pointwise_cartesian_over_laws
      : is_nat_trans
          _ _
          is_cartesian_2cell_sfib_pointwise_cartesian_over_data.
    Show proof.
      intros x y f ; cbn.
      refine (!_).
      use z_iso_inv_on_right.
      rewrite !assoc.
      use z_iso_inv_on_left.
      rewrite cartesian_factorization_sfib_over.
      rewrite !assoc'.
      apply maponpaths.
      rewrite z_iso_after_z_iso_inv.
      rewrite id_right.
      apply idpath.

    Definition is_cartesian_2cell_sfib_pointwise_cartesian_over
      : G₁ ∙ F ⟹ pointwise_lift_functor ∙ F.
    Show proof.
      use make_nat_trans.
      - exact is_cartesian_2cell_sfib_pointwise_cartesian_over_data.
      - exact is_cartesian_2cell_sfib_pointwise_cartesian_over_laws.

    Definition is_cartesian_2cell_sfib_pointwise_cartesian_inv2cell
      : invertible_2cell (G₁ · F) (pointwise_lift_functor · F).
    Show proof.
      use nat_z_iso_to_invertible_2cell.
      use make_nat_z_iso.
      - exact is_cartesian_2cell_sfib_pointwise_cartesian_over.
      - intro.
        apply z_iso_is_z_isomorphism.

    Definition is_cartesian_2cell_sfib_pointwise_cartesian_eq
      : α ▹ F
        =
        is_cartesian_2cell_sfib_pointwise_cartesian_inv2cell
        • (pointwise_lift_nat_trans ▹ F).
    Show proof.
      use nat_trans_eq.
      {
        apply homset_property.
      }
      intro x.
      simpl.
      unfold pointwise_lift_nat_trans_data.
      refine (!_).
      etrans.
      {
        apply maponpaths.
        exact (pr122 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))).
      }
      rewrite !assoc.
      etrans.
      {
        apply maponpaths_2.
        apply z_iso_after_z_iso_inv.
      }
      apply id_left.

    Definition is_cartesian_2cell_sfib_pointwise_cartesian
               (x : pr1 C₀)
      : is_cartesian_sfib F (pr1 α x).
    Show proof.
      pose (i := invertible_between_cartesians
                   Hα
                   pointwise_lift_nat_trans_is_cartesian_2cell
                   is_cartesian_2cell_sfib_pointwise_cartesian_inv2cell
                   is_cartesian_2cell_sfib_pointwise_cartesian_eq).
      use is_cartesian_sfib_eq.
      - exact (nat_z_iso_pointwise_z_iso (invertible_2cell_to_nat_z_iso _ _ i) x
              · pr1 pointwise_lift_nat_trans x).
      - exact (cartesian_factorization_sfib_commute _ _ _ _ _).
      - use comp_is_cartesian_sfib.
        + apply z_iso_is_cartesian_sfib.
          apply z_iso_is_z_isomorphism.
        + exact (pr222 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))).
  End IsCartesian.

  Definition street_fib_is_internal_sfib_lwhisker_is_cartesian
    : lwhisker_is_cartesian F.
  Show proof.
    intros C₀ C₀' G H₁ H₂ α Hα.
    use pointwise_cartesian_is_cartesian.
    intro x ; cbn.
    apply is_cartesian_2cell_sfib_pointwise_cartesian.
    exact Hα.

  Definition street_fib_is_internal_sfib
    : internal_sfib F.
  Show proof.
    split.
    - exact street_fib_is_internal_sfib_cleaving.
    - exact street_fib_is_internal_sfib_lwhisker_is_cartesian.
End StreetFibToInternalSFib.

Definition internal_sfib_weq_street_fib
           {C₁ C₂ : bicat_of_univ_cats}
           (F : C₁ --> C₂)
  : internal_sfib F ≃ street_fib F.
Show proof.
  use weqimplimpl.
  - exact internal_sfib_is_street_fib.
  - exact street_fib_is_internal_sfib.
  - apply isaprop_internal_sfib.
    exact univalent_cat_is_univalent_2_1.
  - apply isaprop_street_fib.
    apply C₁.

2. Internal Street Opfibrations
Section InternalSOpFibToStreetOpFib.
  Context {C₁ C₂ : bicat_of_univ_cats}
          {F : C₁ --> C₂}
          (HF : internal_sopfib F).

  Section InternalSOpFibToStreetOpFibFactor.
    Context {G₁ G₂ : (unit_category : bicat_of_univ_cats) --> C₁}
            {α : G₁ ==> G₂}
            (Hα : is_opcartesian_2cell_sopfib F α)
            {z : pr1 C₁}
            {g : pr1 G₁ tt --> z}
            {h : pr1 F (pr1 G₂ tt) --> pr1 F z}
            (q : # (pr1 F) g = # (pr1 F) (pr1 α tt) · h).

    Let Φ : unit_category ⟶ pr1 C₁
      := functor_from_unit z.

    Local Definition internal_sopfib_is_opcartesian_sopfib_factor_nat_trans_1
      : pr1 G₁ ⟹ Φ.
    Show proof.
      use make_nat_trans.
      - intro x ; induction x.
        exact g.
      - abstract
          (intros x y f ; cbn ;
           induction x ; induction y ;
           cbn ;
           assert (p : f = identity _) ; [ apply isapropunit | ] ;
           rewrite p ;
           rewrite (functor_id G₁) ;
           rewrite id_left, id_right ;
           apply idpath).

    Let ζ := internal_sopfib_is_opcartesian_sopfib_factor_nat_trans_1.

    Local Definition internal_sopfib_is_opcartesian_sopfib_factor_nat_trans_2
      : G₂ · F ==> Φ ∙ F.
    Show proof.
      use make_nat_trans.
      - intros x ; induction x.
        exact h.
      - abstract
          (intros x y f ; cbn ;
           induction x ; induction y ;
           cbn ;
           assert (p : f = identity _) ; [ apply isapropunit | ] ;
           rewrite p ;
           rewrite (functor_id G₂) ;
           rewrite !(functor_id F) ;
           rewrite id_left, id_right ;
           apply idpath).

    Let ξ := internal_sopfib_is_opcartesian_sopfib_factor_nat_trans_2.

    Local Lemma internal_sopfib_is_opcartesian_sopfib_factor_eq
      : post_whisker ζ F
        =
        nat_trans_comp _ _ _ (post_whisker α F) ξ.
    Show proof.
      use nat_trans_eq.
      {
        apply homset_property.
      }
      intro x ; induction x.
      exact q.

    Let p := internal_sopfib_is_opcartesian_sopfib_factor_eq.

    Definition internal_sopfib_is_opcartesian_sopfib_factor
      : pr1 G₂ tt --> z
      := pr1 (is_opcartesian_2cell_sopfib_factor _ Hα ζ ξ p) tt.

    Definition internal_sopfib_is_opcartesian_sopfib_factor_over
      : # (pr1 F) internal_sopfib_is_opcartesian_sopfib_factor = h.
    Show proof.
      exact (nat_trans_eq_pointwise
               (is_opcartesian_2cell_sopfib_factor_over _ Hα _ _ p)
               tt).

    Definition internal_sopfib_is_opcartesian_sopfib_factor_comm
      : pr1 α tt · internal_sopfib_is_opcartesian_sopfib_factor = g.
    Show proof.
      exact (nat_trans_eq_pointwise
               (is_opcartesian_2cell_sopfib_factor_comm _ Hα _ _ p)
               tt).

    Local Definition internal_sopfib_is_opcartesian_sopfib_factor_unique_help
               (k : pr1 G₂ tt --> z)
      : pr1 G₂ ⟹ Φ.
    Show proof.
      use make_nat_trans.
      - intro x ; induction x.
        exact k.
      - abstract
          (intros x y f ;
           induction x ; induction y ; cbn ;
           assert (r : f = identity _) ; [ apply isapropunit | ] ;
           rewrite r ;
           rewrite !(functor_id G₂) ;
           rewrite id_left, id_right ;
           apply idpath).

    Definition internal_sopfib_is_opcartesian_sopfib_factor_unique
      : isaprop (∑ φ, # (pr1 F) φ = h × pr1 α tt · φ = g).
    Show proof.
      use invproofirrelevance.
      intros φ₁ φ₂.
      use subtypePath.
      {
        intro.
        apply isapropdirprod ; apply homset_property.
      }
      refine (nat_trans_eq_pointwise
                (is_opcartesian_2cell_sopfib_factor_unique
                   _ Hα
                   Φ ζ ξ p
                   (internal_sopfib_is_opcartesian_sopfib_factor_unique_help (pr1 φ₁))
                   (internal_sopfib_is_opcartesian_sopfib_factor_unique_help (pr1 φ₂))
                   _ _ _ _)
                tt) ;
        (use nat_trans_eq ; [ apply homset_property | ]) ;
        intro x ; induction x ; cbn.
      - exact (pr12 φ₁).
      - exact (pr12 φ₂).
      - exact (pr22 φ₁).
      - exact (pr22 φ₂).
  End InternalSOpFibToStreetOpFibFactor.

  Definition internal_sopfib_is_opcartesian_sopfib
             {G₁ G₂ : (unit_category : bicat_of_univ_cats) --> C₁}
             {α : G₁ ==> G₂}
             (Hα : is_opcartesian_2cell_sopfib F α)
    : is_opcartesian_sopfib F (pr1 α tt).
  Show proof.
    intros z g h q.
    use iscontraprop1.
    - exact (internal_sopfib_is_opcartesian_sopfib_factor_unique Hα q).
    - simple refine (_ ,, _ ,, _).
      + exact (internal_sopfib_is_opcartesian_sopfib_factor Hα q).
      + exact (internal_sopfib_is_opcartesian_sopfib_factor_over Hα q).
      + exact (internal_sopfib_is_opcartesian_sopfib_factor_comm Hα q).

  Section OpCleaving.
    Context {e : pr1 C₁}
            {b : pr1 C₂}
            (f : pr1 F e --> b).

    Definition internal_sopfib_is_street_opfib_nat_trans
      : functor_from_unit e ∙ F ⟹ functor_from_unit b.
    Show proof.
      use make_nat_trans.
      - exact (λ _, f).
      - abstract
          (intros z₁ z₂ g ; cbn ;
           rewrite functor_id, id_left, id_right ;
           apply idpath).

    Let ℓ := pr1 HF _ _ _ internal_sopfib_is_street_opfib_nat_trans.

    Definition internal_sopfib_is_street_opfib_lift_ob
      : pr1 C₁
      := pr1 (pr1 ℓ) tt.

    Definition internal_sopfib_is_street_opfib_lift_mor
      : e --> internal_sopfib_is_street_opfib_lift_ob
      := pr1 (pr12 ℓ) tt.

    Definition internal_sopfib_is_street_opfib_lift_z_iso
      : z_iso b (pr1 F internal_sopfib_is_street_opfib_lift_ob)
      := nat_z_iso_pointwise_z_iso (invertible_2cell_to_nat_z_iso _ _ (pr122 ℓ)) tt.

    Definition internal_sopfib_is_street_opfib_lift_over
      : # (pr1 F) internal_sopfib_is_street_opfib_lift_mor
        =
        f · internal_sopfib_is_street_opfib_lift_z_iso
      := nat_trans_eq_pointwise (pr2 (pr222 ℓ)) tt.

    Definition internal_sopfib_is_street_opfib_lift_cartesian
      : is_opcartesian_sopfib F internal_sopfib_is_street_opfib_lift_mor
      := internal_sopfib_is_opcartesian_sopfib (pr1 (pr222 ℓ)).
  End OpCleaving.

  Definition internal_sopfib_is_street_opfib
    : street_opfib F.
  Show proof.
    intros e b f.
    simple refine (_ ,, (_ ,, _) ,, _ ,, _) ; cbn.
    - exact (internal_sopfib_is_street_opfib_lift_ob f).
    - exact (internal_sopfib_is_street_opfib_lift_mor f).
    - exact (internal_sopfib_is_street_opfib_lift_z_iso f).
    - exact (internal_sopfib_is_street_opfib_lift_over f).
    - exact (internal_sopfib_is_street_opfib_lift_cartesian f).
End InternalSOpFibToStreetOpFib.

Section StreetOpFibToInternalSOpFib.
  Context {C₁ C₂ : bicat_of_univ_cats}
          {F : C₁ --> C₂}
          (HF : street_opfib F).

  Section IsOpCartesian.
    Context {C₀ : bicat_of_univ_cats}
            {G₁ G₂ : C₀ --> C₁}
            (α : G₁ ==> G₂)
            (Hα : ∏ (x : pr1 C₀), is_opcartesian_sopfib F (pr1 α x)).

    Section Factorization.
      Context {H : C₀ --> C₁}
              {β : G₁ ==> H}
              {δp : G₂ · F ==> H · F}
              (q : β ▹ F = (α ▹ F) • δp).

      Definition pointwise_opcartesian_is_opcartesian_factor_data
        : nat_trans_data (pr1 G₂) (pr1 H)
        := λ x,
           opcartesian_factorization_sopfib
             _
             (Hα x)
             (pr1 β x)
             (pr1 δp x)
             (nat_trans_eq_pointwise q x).

      Definition pointwise_opcartesian_is_opcartesian_factor_laws
        : is_nat_trans _ _ pointwise_opcartesian_is_opcartesian_factor_data.
      Show proof.
        intros x y f ; unfold pointwise_opcartesian_is_opcartesian_factor_data ; cbn.
        pose (opcartesian_factorization_sopfib_commute
                F
                (Hα x) (pr1 β x) (pr1 δp x)
                (nat_trans_eq_pointwise q x))
          as p.
        pose (opcartesian_factorization_sopfib_commute
                F
                (Hα y) (pr1 β y) (pr1 δp y)
                (nat_trans_eq_pointwise q y))
          as p'.
        use (opcartesian_factorization_sopfib_unique
               _
               (Hα x)
               (pr1 β x · # (pr1 H) f)
               (pr1 δp x · # (pr1 F) (# (pr1 H) f))).
        - rewrite functor_comp.
          pose (r := nat_trans_eq_pointwise q x) ; cbn in r.
          etrans.
          {
            apply maponpaths_2.
            exact r.
          }
          clear r.
          rewrite !assoc'.
          apply idpath.
        - rewrite functor_comp.
          rewrite opcartesian_factorization_sopfib_over.
          exact (nat_trans_ax δp _ _ f).
        - rewrite !functor_comp.
          rewrite opcartesian_factorization_sopfib_over.
          apply idpath.
        - rewrite !assoc.
          etrans.
          {
            apply maponpaths_2.
            exact (!(nat_trans_ax α _ _ f)).
          }
          rewrite !assoc'.
          etrans.
          {
            apply maponpaths.
            exact p'.
          }
          exact (nat_trans_ax β _ _ f).
        - rewrite !assoc.
          apply maponpaths_2.
          exact p.

      Definition pointwise_opcartesian_is_opcartesian_factor
        : G₂ ==> H.
      Show proof.
        use make_nat_trans.
        - exact pointwise_opcartesian_is_opcartesian_factor_data.
        - exact pointwise_opcartesian_is_opcartesian_factor_laws.

      Definition pointwise_opcartesian_is_opcartesian_over
        : pointwise_opcartesian_is_opcartesian_factor ▹ F = δp.
      Show proof.
        use nat_trans_eq.
        {
          apply homset_property.
        }
        intro x ; cbn.
        apply opcartesian_factorization_sopfib_over.

      Definition pointwise_opcartesian_is_opcartesian_comm
        : α • pointwise_opcartesian_is_opcartesian_factor = β.
      Show proof.
        use nat_trans_eq.
        {
          apply homset_property.
        }
        intro x ; cbn.
        apply opcartesian_factorization_sopfib_commute.

      Definition pointwise_opcartesian_is_opcartesian_unique
        : isaprop (∑ (δ : G₂ ==> H), δ ▹ F = δp × α • δ = β).
      Show proof.
        use invproofirrelevance.
        intros δ₁ δ₂.
        use subtypePath.
        {
          intro.
          apply isapropdirprod ; apply cellset_property.
        }
        use nat_trans_eq.
        {
          apply homset_property.
        }
        intro x.
        use (opcartesian_factorization_sopfib_unique
               _ (Hα x)
               (pr1 β x)
               (pr1 δp x)).
        - exact (nat_trans_eq_pointwise q x).
        - exact (nat_trans_eq_pointwise (pr12 δ₁) x).
        - exact (nat_trans_eq_pointwise (pr12 δ₂) x).
        - exact (nat_trans_eq_pointwise (pr22 δ₁) x).
        - exact (nat_trans_eq_pointwise (pr22 δ₂) x).
    End Factorization.

    Definition pointwise_opcartesian_is_opcartesian
      : is_opcartesian_2cell_sopfib F α.
    Show proof.
      intros H β δp q.
      use iscontraprop1.
      - exact (pointwise_opcartesian_is_opcartesian_unique q).
      - simple refine (_ ,, _ ,, _).
        + exact (pointwise_opcartesian_is_opcartesian_factor q).
        + exact (pointwise_opcartesian_is_opcartesian_over q).
        + exact (pointwise_opcartesian_is_opcartesian_comm q).
  End IsOpCartesian.

  Section OpCleaving.
    Context {C₀ : bicat_of_univ_cats}
            {G₁ : C₀ --> C₁}
            {G₂ : C₀ --> C₂}
            (α : G₁ · F ==> G₂).

    Definition street_opfib_is_internal_sopfib_opcleaving_lift_data
      : functor_data (pr1 C₀) (pr1 C₁).
    Show proof.
      use make_functor_data.
      - exact (λ x, pr1 (HF _ _ (pr1 α x))).
      - intros x y f ; cbn.
        use (opcartesian_factorization_sopfib
               _
               (pr222 (HF _ _ (pr1 α x)))).
        + exact (# (pr1 G₁) f · pr112 (HF _ _ (pr1 α y))).
        + exact (inv_from_z_iso (pr212 (HF _ _ (pr1 α x)))
                 · # (pr1 G₂) f
                 · pr212 (HF _ _ (pr1 α y))).
        + abstract
            (rewrite functor_comp ;
             rewrite (pr122 (HF _ _ (pr1 α x))) ;
             refine (maponpaths (λ z, _ · z) (pr122 (HF _ _ (pr1 α y))) @ _) ;
             rewrite !assoc ;
             apply maponpaths_2 ;
             refine (nat_trans_ax α _ _ f @ _) ;
             rewrite !assoc' ;
             apply maponpaths ;
             rewrite !assoc ;
             rewrite z_iso_inv_after_z_iso ;
             rewrite id_left ;
             apply idpath).

    Definition street_opfib_is_internal_sopfib_opcleaving_lift_is_functor
      : is_functor street_opfib_is_internal_sopfib_opcleaving_lift_data.
    Show proof.
      split.
      - intro x ; cbn.
        use (opcartesian_factorization_sopfib_unique
               _
               (pr222 (HF _ _ (pr1 α x)))).
        + exact (pr112 (HF _ _ (pr1 α x))).
        + apply identity.
        + rewrite id_right.
          apply idpath.
        + rewrite opcartesian_factorization_sopfib_over.
          refine (!_).
          rewrite (functor_id G₂).
          rewrite id_right.
          rewrite z_iso_after_z_iso_inv.
          apply idpath.
        + apply functor_id.
        + rewrite opcartesian_factorization_sopfib_commute.
          rewrite (functor_id G₁).
          apply id_left.
        + apply id_right.
      - intros x y z f g ; cbn.
        use (opcartesian_factorization_sopfib_unique
               _
               (pr222 (HF _ _ (pr1 α x)))).
        + exact (# (pr1 G₁) (f · g) · pr112 (HF _ _ (pr1 α z))).
        + exact (inv_from_z_iso (pr212 (HF _ _ (pr1 α x)))
                 · # (pr1 G₂) (f · g)
                 · pr212 (HF _ _ (pr1 α z))).
        + rewrite functor_comp.
          etrans.
          {
            apply maponpaths.
            exact (pr122 (HF _ _ (pr1 α z))).
          }
          rewrite !assoc.
          apply maponpaths_2.
          refine (nat_trans_ax α _ _ (f · g) @ _).
          apply maponpaths_2.
          use z_iso_inv_on_left.
          exact (pr122 (HF _ _ (pr1 α x))).
        + apply opcartesian_factorization_sopfib_over.
        + rewrite functor_comp.
          rewrite !opcartesian_factorization_sopfib_over.
          rewrite !assoc'.
          apply maponpaths.
          rewrite !assoc.
          apply maponpaths_2.
          rewrite (functor_comp G₂).
          rewrite !assoc'.
          apply maponpaths.
          rewrite !assoc.
          rewrite z_iso_inv_after_z_iso.
          apply id_left.
        + apply opcartesian_factorization_sopfib_commute.
        + rewrite !assoc.
          rewrite opcartesian_factorization_sopfib_commute.
          rewrite !assoc'.
          rewrite opcartesian_factorization_sopfib_commute.
          rewrite !assoc.
          rewrite (functor_comp G₁).
          apply idpath.

    Definition street_opfib_is_internal_sopfib_opcleaving_lift
      : C₀ --> C₁.
    Show proof.
      use make_functor.
      - exact street_opfib_is_internal_sopfib_opcleaving_lift_data.
      - exact street_opfib_is_internal_sopfib_opcleaving_lift_is_functor.

    Definition street_opfib_is_internal_sopfib_opcleaving_lift_mor_data
      : nat_trans_data
          (pr1 G₁)
          street_opfib_is_internal_sopfib_opcleaving_lift_data
      := λ x, pr112 (HF _ _ (pr1 α x)).

    Definition street_opfib_is_internal_sopfib_opcleaving_lift_mor_is_nat_trans
      : is_nat_trans _ _ street_opfib_is_internal_sopfib_opcleaving_lift_mor_data.
    Show proof.
      intros x y f ; cbn.
      refine (!_).
      apply opcartesian_factorization_sopfib_commute.

    Definition street_opfib_is_internal_sopfib_opcleaving_lift_mor
      : G₁ ==> street_opfib_is_internal_sopfib_opcleaving_lift.
    Show proof.
      use make_nat_trans.
      - exact street_opfib_is_internal_sopfib_opcleaving_lift_mor_data.
      - exact street_opfib_is_internal_sopfib_opcleaving_lift_mor_is_nat_trans.

    Definition street_opfib_is_internal_sopfib_opcleaving_lift_over_nat_trans_data
      : nat_trans_data (pr1 G₂) (street_opfib_is_internal_sopfib_opcleaving_lift ∙ F)
      := λ x, pr212 (HF _ _ (pr1 α x)).

    Definition street_opfib_is_internal_sopfib_opcleaving_lift_over_is_nat_trans
      : is_nat_trans
          _ _
          street_opfib_is_internal_sopfib_opcleaving_lift_over_nat_trans_data.
    Show proof.
      intros x y f ; cbn.
      unfold street_opfib_is_internal_sopfib_opcleaving_lift_over_nat_trans_data.
      rewrite opcartesian_factorization_sopfib_over.
      rewrite !assoc.
      rewrite z_iso_inv_after_z_iso.
      rewrite id_left.
      apply idpath.

    Definition street_opfib_is_internal_sopfib_opcleaving_lift_over_nat_trans
      : pr1 G₂ ⟹ street_opfib_is_internal_sopfib_opcleaving_lift ∙ F.
    Show proof.
      use make_nat_trans.
      - exact street_opfib_is_internal_sopfib_opcleaving_lift_over_nat_trans_data.
      - exact street_opfib_is_internal_sopfib_opcleaving_lift_over_is_nat_trans.

    Definition street_opfib_is_internal_sopfib_opcleaving_lift_opcartesian
      : is_opcartesian_2cell_sopfib
          F
          street_opfib_is_internal_sopfib_opcleaving_lift_mor.
    Show proof.
      use pointwise_opcartesian_is_opcartesian.
      intro x.
      exact (pr222 (HF _ _ (pr1 α x))).

    Definition street_opfib_is_internal_sopfib_opcleaving_lift_over
      : invertible_2cell
          G₂
          (street_opfib_is_internal_sopfib_opcleaving_lift · F).
    Show proof.
      use nat_z_iso_to_invertible_2cell.
      use make_nat_z_iso.
      - exact street_opfib_is_internal_sopfib_opcleaving_lift_over_nat_trans.
      - intro x.
        apply z_iso_is_z_isomorphism.
  End OpCleaving.

  Definition street_opfib_is_internal_sopfib_opcleaving
    : internal_sopfib_opcleaving F.
  Show proof.
    intros C₀ G₁ G₂ α.
    simple refine (_ ,, _ ,, _ ,, _ ,, _).
    - exact (street_opfib_is_internal_sopfib_opcleaving_lift α).
    - exact (street_opfib_is_internal_sopfib_opcleaving_lift_mor α).
    - exact (street_opfib_is_internal_sopfib_opcleaving_lift_over α).
    - exact (street_opfib_is_internal_sopfib_opcleaving_lift_opcartesian α).
    - abstract
        (use nat_trans_eq ; [ apply homset_property | ] ;
         intro x ; cbn ;
         exact (pr122 (HF _ _ (pr1 α x)))).

  Section IsOpCartesian.
    Context {C₀ : bicat_of_univ_cats}
            {G₁ G₂ : C₀ --> C₁}
            (α : G₁ ==> G₂)
            (Hα : is_opcartesian_2cell_sopfib F α).

    Definition pointwise_oplift_functor_data
      : functor_data (pr1 C₀) (pr1 C₁).
    Show proof.
      use make_functor_data.
      - exact (λ x, pr1 (HF _ _ (# (pr1 F) (pr1 α x)))).
      - intros x y f ; cbn.
        use (opcartesian_factorization_sopfib
               _
               (pr222 (HF _ _ (# (pr1 F) (pr1 α x))))).
        + exact (# (pr1 G₁) f · pr112 (HF _ _ (# (pr1 F) (pr1 α y)))).
        + exact (inv_from_z_iso (pr212 (HF _ _ (# (pr1 F) (pr1 α x))))
                 · # (pr1 F) (# (pr1 G₂) f)
                 · pr212 (HF _ _ (# (pr1 F) (pr1 α y)))).
        + abstract
            (rewrite functor_comp ;
             rewrite (pr122 (HF _ _ (# (pr1 F) (pr1 α x)))) ;
             rewrite !assoc ;
             etrans ;
             [ apply maponpaths ;
               exact (pr122 (HF _ _ (# (pr1 F) (pr1 α y))))
             | ] ;
             rewrite !assoc ;
             apply maponpaths_2 ;
             rewrite <- !functor_comp ;
             etrans ;
             [ apply maponpaths ;
               exact (nat_trans_ax α _ _ f)
             | ] ;
             rewrite functor_comp ;
             rewrite !assoc' ;
             apply maponpaths ;
             rewrite !assoc ;
             rewrite z_iso_inv_after_z_iso ;
             rewrite id_left ;
             apply idpath).

    Definition pointwise_oplift_functor_is_functor
      : is_functor pointwise_oplift_functor_data.
    Show proof.
      split.
      - intro x ; cbn.
        use (opcartesian_factorization_sopfib_unique
               _
               (pr222 (HF _ _ (# (pr1 F) (pr1 α x))))).
        + exact (pr112 (HF _ _ (# (pr1 F) (pr1 α x)))).
        + apply identity.
        + rewrite id_right.
          apply idpath.
        + rewrite opcartesian_factorization_sopfib_over.
          rewrite !assoc'.
          use z_iso_inv_on_right.
          rewrite id_right.
          rewrite (functor_id G₂).
          rewrite (functor_id F).
          apply id_left.
        + apply functor_id.
        + rewrite opcartesian_factorization_sopfib_commute.
          rewrite (functor_id G₁).
          apply id_left.
        + apply id_right.
      - intros x y z f g ; cbn.
        use (opcartesian_factorization_sopfib_unique
               _
               (pr222 (HF _ _ (# (pr1 F) (pr1 α x))))).
        + exact (# (pr1 G₁) (f · g)
                 · pr112 (HF _ _ (# (pr1 F) (pr1 α z)))).
        + exact (inv_from_z_iso
                   (pr212 (HF _ _ (# (pr1 F) (pr1 α x))))
                 · # (pr1 F) (# (pr1 G₂) (f · g))
                 · pr212 (HF _ _ (# (pr1 F) (pr1 α z)))).
        + rewrite functor_comp.
          rewrite (pr122 (HF _ _ (# (pr1 F) (pr1 α x)))).
          etrans.
          {
            apply maponpaths.
            exact (pr122 (HF _ _ (# (pr1 F) (pr1 α z)))).
          }
          rewrite !assoc.
          rewrite <- (functor_comp F).
          etrans.
          {
            apply maponpaths_2.
            apply maponpaths.
            exact (nat_trans_ax α _ _ (f · g)).
          }
          rewrite functor_comp.
          rewrite !assoc'.
          apply maponpaths.
          rewrite !assoc.
          apply maponpaths_2.
          rewrite z_iso_inv_after_z_iso.
          rewrite id_left.
          apply idpath.
        + apply opcartesian_factorization_sopfib_over.
        + rewrite functor_comp.
          rewrite !opcartesian_factorization_sopfib_over.
          rewrite (functor_comp G₂).
          rewrite (functor_comp F).
          rewrite !assoc'.
          do 2 apply maponpaths.
          rewrite !assoc.
          apply maponpaths_2.
          rewrite z_iso_inv_after_z_iso.
          apply id_left.
        + apply opcartesian_factorization_sopfib_commute.
        + rewrite !assoc.
          rewrite opcartesian_factorization_sopfib_commute.
          rewrite !assoc'.
          rewrite opcartesian_factorization_sopfib_commute.
          rewrite !assoc.
          rewrite (functor_comp G₁).
          apply idpath.

    Definition pointwise_oplift_functor
      : C₀ --> C₁.
    Show proof.
      use make_functor.
      - exact pointwise_oplift_functor_data.
      - exact pointwise_oplift_functor_is_functor.

    Definition pointwise_oplift_nat_trans_data
      : nat_trans_data (pr1 G₁) pointwise_oplift_functor_data
      := λ x, pr112 (HF _ _ (# (pr1 F) (pr1 α x))).

    Definition pointwise_oplift_is_nat_trans
      : is_nat_trans _ _ pointwise_oplift_nat_trans_data.
    Show proof.
      intros x y f ; cbn.
      unfold pointwise_oplift_nat_trans_data.
      refine (!_).
      apply opcartesian_factorization_sopfib_commute.

    Definition pointwise_oplift_nat_trans
      : G₁ ==> pointwise_oplift_functor.
    Show proof.
      use make_nat_trans.
      - exact pointwise_oplift_nat_trans_data.
      - exact pointwise_oplift_is_nat_trans.

    Definition pointwise_oplift_nat_trans_is_opcartesian_2cell
      : is_opcartesian_2cell_sopfib F pointwise_oplift_nat_trans.
    Show proof.
      use pointwise_opcartesian_is_opcartesian.
      intro x.
      exact (pr222 (HF _ _ (# (pr1 F) (pr1 α x)))).

    Definition is_opcartesian_2cell_sopfib_pointwise_opcartesian_over_data
      : nat_trans_data (pointwise_oplift_functor ∙ F) (G₂ ∙ F).
    Show proof.
      intro x.
      pose (i := pr212 (HF _ _ (# (pr1 F) (pr1 α x)))).
      exact (z_iso_inv_from_z_iso i).

    Definition is_opcartesian_2cell_sopfib_pointwise_opcartesian_over_laws
      : is_nat_trans
          _ _
          is_opcartesian_2cell_sopfib_pointwise_opcartesian_over_data.
    Show proof.
      intros x y f ; cbn.
      refine (!_).
      use z_iso_inv_on_right.
      rewrite !assoc.
      use z_iso_inv_on_left.
      rewrite opcartesian_factorization_sopfib_over.
      rewrite !assoc.
      apply maponpaths_2.
      rewrite z_iso_inv_after_z_iso.
      rewrite id_left.
      apply idpath.

    Definition is_opcartesian_2cell_sopfib_pointwise_opcartesian_over
      : pointwise_oplift_functor ∙ F ⟹ G₂ ∙ F.
    Show proof.
      use make_nat_trans.
      - exact is_opcartesian_2cell_sopfib_pointwise_opcartesian_over_data.
      - exact is_opcartesian_2cell_sopfib_pointwise_opcartesian_over_laws.

    Definition is_opcartesian_2cell_sopfib_pointwise_opcartesian_inv2cell
      : invertible_2cell (pointwise_oplift_functor · F) (G₂ · F).
    Show proof.
      use nat_z_iso_to_invertible_2cell.
      use make_nat_z_iso.
      - exact is_opcartesian_2cell_sopfib_pointwise_opcartesian_over.
      - intro.
        apply z_iso_is_z_isomorphism.

    Definition is_opcartesian_2cell_sopfib_pointwise_opcartesian_eq
      : α ▹ F
        =
        (pointwise_oplift_nat_trans ▹ F)
        • is_opcartesian_2cell_sopfib_pointwise_opcartesian_inv2cell.
    Show proof.
      use nat_trans_eq.
      {
        apply homset_property.
      }
      intro x.
      cbn.
      unfold pointwise_oplift_nat_trans_data.
      refine (!_).
      etrans.
      {
        apply maponpaths_2.
        exact (pr122 (HF _ _ (# (pr1 F) (pr1 α x)))).
      }
      rewrite !assoc'.
      etrans.
      {
        apply maponpaths.
        apply z_iso_inv_after_z_iso.
      }
      apply id_right.

    Definition is_opcartesian_2cell_sfib_pointwise_opcartesian
               (x : pr1 C₀)
      : is_opcartesian_sopfib F (pr1 α x).
    Show proof.
      pose (i := invertible_between_opcartesians
                   Hα
                   pointwise_oplift_nat_trans_is_opcartesian_2cell
                   is_opcartesian_2cell_sopfib_pointwise_opcartesian_inv2cell
                   is_opcartesian_2cell_sopfib_pointwise_opcartesian_eq).
      use is_opcartesian_sopfib_eq.
      - exact (pr1 pointwise_oplift_nat_trans x
               · nat_z_iso_pointwise_z_iso (invertible_2cell_to_nat_z_iso _ _ i) x).
      - exact (opcartesian_factorization_sopfib_commute _ _ _ _ _).
      - use comp_is_opcartesian_sopfib.
        + exact (pr222 (HF _ _ (# (pr1 F) (pr1 α x)))).
        + apply iso_is_opcartesian_sopfib.
          apply z_iso_is_z_isomorphism.
  End IsOpCartesian.

  Definition street_opfib_is_internal_sopfib_lwhisker_is_opcartesian
    : lwhisker_is_opcartesian F.
  Show proof.
    intros C₀ C₀' G H₁ H₂ α Hα.
    use pointwise_opcartesian_is_opcartesian.
    intro x ; cbn.
    apply is_opcartesian_2cell_sfib_pointwise_opcartesian.
    exact Hα.

  Definition street_opfib_is_internal_sopfib
    : internal_sopfib F.
  Show proof.
    split.
    - exact street_opfib_is_internal_sopfib_opcleaving.
    - exact street_opfib_is_internal_sopfib_lwhisker_is_opcartesian.
End StreetOpFibToInternalSOpFib.

Definition internal_sopfib_weq_street_opfib
           {C₁ C₂ : bicat_of_univ_cats}
           (F : C₁ --> C₂)
  : internal_sopfib F ≃ street_opfib F.
Show proof.
  use weqimplimpl.
  - exact internal_sopfib_is_street_opfib.
  - exact street_opfib_is_internal_sopfib.
  - apply isaprop_internal_sopfib.
    exact univalent_cat_is_univalent_2_1.
  - apply isaprop_street_opfib.
    apply C₁.