Library UniMath.Bicategories.Morphisms.InternalStreetFibration

1. Definition of an internal Street fibration
We define internal Street fibrations using an unfolded definition. We also show that it is equivalent to the usual definition of internal Street fibrations, which is formulated using hom-categories.
Section InternalStreetFibration.
  Context {B : bicat}
          {e b : B}
          (p : e --> b).

  Definition is_cartesian_2cell_sfib
             {x : B}
             {f g : x --> e}
             (γ : f ==> g)
    : UU
    := (h : x --> e)
         (α : h ==> g)
         (δp : h · p ==> f · p)
         (q : α p = δp (γ p)),
       ∃! (δ : h ==> f),
       δ p = δp
       ×
       δ γ = α.

  Definition is_cartesian_2cell_sfib_factor
             {x : B}
             {f g : x --> e}
             {γ : f ==> g}
             ( : is_cartesian_2cell_sfib γ)
             {h : x --> e}
             (α : h ==> g)
             (δp : h · p ==> f · p)
             (q : α p = δp (γ p))
    : h ==> f
    := pr11 ( h α δp q).

  Definition is_cartesian_2cell_sfib_factor_over
             {x : B}
             {f g : x --> e}
             {γ : f ==> g}
             ( : is_cartesian_2cell_sfib γ)
             {h : x --> e}
             {α : h ==> g}
             {δp : h · p ==> f · p}
             (q : α p = δp (γ p))
    : (is_cartesian_2cell_sfib_factor _ _ q) p = δp
    := pr121 ( h α δp q).

  Definition is_cartesian_2cell_sfib_factor_comm
             {x : B}
             {f g : x --> e}
             {γ : f ==> g}
             ( : is_cartesian_2cell_sfib γ)
             {h : x --> e}
             {α : h ==> g}
             {δp : h · p ==> f · p}
             (q : α p = δp (γ p))
    : is_cartesian_2cell_sfib_factor _ _ q γ = α
    := pr221 ( h α δp q).

  Definition is_cartesian_2cell_sfib_factor_unique
             {x : B}
             {f g : x --> e}
             {γ : f ==> g}
             ( : is_cartesian_2cell_sfib γ)
             (h : x --> e)
             (α : h ==> g)
             (δp : h · p ==> f · p)
             (q : α p = δp (γ p))
             (δ₁ δ₂ : h ==> f)
             (pδ₁ : δ₁ p = δp)
             (pδ₂ : δ₂ p = δp)
             (δγ₁ : δ₁ γ = α)
             (δγ₂ : δ₂ γ = α)
    : δ₁ = δ₂.
  Show proof.
    pose (proofirrelevance
            _
            (isapropifcontr ( h α δp q))
            (δ₁ ,, pδ₁ ,, δγ₁)
            (δ₂ ,, pδ₂ ,, δγ₂))
      as H.
    exact (maponpaths pr1 H).

  Definition isaprop_is_cartesian_2cell_sfib
             {x : B}
             {f : x --> e}
             {g : x --> e}
             (γ : f ==> g)
    : isaprop (is_cartesian_2cell_sfib γ).
  Show proof.
    do 4 (use impred ; intro).
    apply isapropiscontr.

  Definition internal_sfib_cleaving
    : UU
    := (x : B)
         (f : x --> b)
         (g : x --> e)
         (α : f ==> g · p),
        (h : x --> e)
         (γ : h ==> g)
         (β : invertible_2cell (h · p) f),
       is_cartesian_2cell_sfib γ
       ×
       γ p = β α.

  Definition internal_sfib_cleaving_lift_mor
             (H : internal_sfib_cleaving)
             {x : B}
             {f : x --> b}
             {g : x --> e}
             (α : f ==> g · p)
    : x --> e
    := pr1 (H _ _ _ α).

  Definition internal_sfib_cleaving_lift_cell
             (H : internal_sfib_cleaving)
             {x : B}
             {f : x --> b}
             {g : x --> e}
             (α : f ==> g · p)
    : internal_sfib_cleaving_lift_mor H α ==> g
    := pr12 (H _ _ _ α).

  Definition internal_sfib_cleaving_com
             (H : internal_sfib_cleaving)
             {x : B}
             {f : x --> b}
             {g : x --> e}
             (α : f ==> g · p)
    : invertible_2cell (internal_sfib_cleaving_lift_mor H α · p) f
    := pr122 (H _ _ _ α).

  Definition internal_sfib_cleaving_is_cartesian
             (H : internal_sfib_cleaving)
             {x : B}
             {f : x --> b}
             {g : x --> e}
             (α : f ==> g · p)
    : is_cartesian_2cell_sfib (internal_sfib_cleaving_lift_cell H α)
    := pr1 (pr222 (H _ _ _ α)).

  Definition internal_sfib_cleaving_over
             (H : internal_sfib_cleaving)
             {x : B}
             {f : x --> b}
             {g : x --> e}
             (α : f ==> g · p)
    : internal_sfib_cleaving_lift_cell H α p
      =
      internal_sfib_cleaving_com H α α
    := pr2 (pr222 (H _ _ _ α)).

  Definition lwhisker_is_cartesian
    : UU
    := (x y : B)
         (h : y --> x)
         (f g : x --> e)
         (γ : f ==> g)
         ( : is_cartesian_2cell_sfib γ),
       is_cartesian_2cell_sfib (h γ).

  Definition internal_sfib
    : UU
    := internal_sfib_cleaving × lwhisker_is_cartesian.

  Coercion internal_sfib_to_cleaving
           (H : internal_sfib)
    : internal_sfib_cleaving
    := pr1 H.

  Definition rep_internal_sfib
    : UU
    := ( (x : B),
        street_fib (post_comp x p))
       ×
       ( (x y : B)
          (h : y --> x),
        preserves_cartesian
          (post_comp x p)
          (post_comp y p)
          (pre_comp e h)).

  Definition rep_internal_sfib_to_internal_sfib
             (H : rep_internal_sfib)
    : internal_sfib.
  Show proof.
    split.
    - intros x f g α.
      pose (lift := pr1 H x g f α).
      exact (pr1 lift
             ,, pr112 lift
             ,, z_iso_to_inv2cell (pr212 lift)
             ,, pr222 lift
             ,, pr122 lift).
    - exact (pr2 H).

  Definition internal_sfib_to_rep_internal_sfib
             (H : internal_sfib)
    : rep_internal_sfib.
  Show proof.
    split.
    - intros x f g α.
      pose (lift := pr1 H x g f α).
      exact (pr1 lift
             ,, (pr12 lift ,, inv2cell_to_z_iso (pr122 lift))
             ,, pr2 (pr222 lift)
             ,, pr1 (pr222 lift)).
    - exact (pr2 H).

  Definition internal_sfib_to_rep_to_sfib
             (H : rep_internal_sfib)
    : internal_sfib_to_rep_internal_sfib
        (rep_internal_sfib_to_internal_sfib H)
      =
      H.
  Show proof.
    use pathsdirprod ; [ | apply idpath ].
    use funextsec ; intro x.
    use funextsec ; intro f.
    use funextsec ; intro g.
    use funextsec ; intro α.
    simpl.
    refine (maponpaths (λ z, _ ,, z) _).
    use subtypePath.
    {
      intro.
      use isapropdirprod.
      - apply cellset_property.
      - apply isaprop_is_cartesian_2cell_sfib.
    }
    simpl.
    refine (maponpaths (λ z, _ ,, z) _).
    use subtypePath.
    {
      intro. apply (isaprop_is_z_isomorphism(C:=hom x b)).
    }
    cbn.
    apply idpath.

  Definition rep_sfib_to_internal_to_rep
             (H : internal_sfib)
    : rep_internal_sfib_to_internal_sfib
        (internal_sfib_to_rep_internal_sfib H)
      =
      H.
  Show proof.
    use pathsdirprod ; [ | apply idpath ].
    use funextsec ; intro x.
    use funextsec ; intro f.
    use funextsec ; intro g.
    use funextsec ; intro α.
    simpl.
    refine (maponpaths (λ z, _ ,, _ ,, z) _).
    use subtypePath.
    {
      intro.
      apply isapropdirprod.
      - apply isaprop_is_cartesian_2cell_sfib.
      - apply cellset_property.
    }
    use subtypePath.
    {
      intro ; apply isaprop_is_invertible_2cell.
    }
    cbn.
    apply idpath.

  Definition rep_internal_sfib_weq_internal_sfib
    : rep_internal_sfib internal_sfib.
  Show proof.
    use make_weq.
    - exact rep_internal_sfib_to_internal_sfib.
    - use isweq_iso.
      + exact internal_sfib_to_rep_internal_sfib.
      + exact internal_sfib_to_rep_to_sfib.
      + exact rep_sfib_to_internal_to_rep.

  Definition isaprop_rep_internal_sfib
             (HB_2_1 : is_univalent_2_1 B)
    : isaprop rep_internal_sfib.
  Show proof.
    use isapropdirprod.
    - use impred ; intro.
      apply isaprop_street_fib.
      apply is_univ_hom.
      exact HB_2_1.
    - do 7 (use impred ; intro).
      apply isaprop_is_cartesian_sfib.

  Definition isaprop_internal_sfib
             (HB_2_1 : is_univalent_2_1 B)
    : isaprop internal_sfib.
  Show proof.
End InternalStreetFibration.

2. Lemmas on cartesians
Definition id_is_cartesian_2cell_sfib
           {B : bicat}
           {e b : B}
           (p : e --> b)
           {x : B}
           (f : x --> e)
  : is_cartesian_2cell_sfib p (id2 f).
Show proof.
  intros g α δp q.
  use iscontraprop1.
  - abstract
      (use invproofirrelevance ;
       intros φ φ ;
       use subtypePath ;
       [ intro ; apply isapropdirprod ; apply cellset_property | ] ;
       exact (!(id2_right _) @ pr22 φ @ !(pr22 φ) @ id2_right _)).
  - refine (α ,, _ ,, _).
    + abstract
        (rewrite q ;
         rewrite id2_rwhisker ;
         apply id2_right).
    + abstract
        (apply id2_right).

Section VcompIsCartesian.
  Context {B : bicat}
          {e b : B}
          (p : e --> b)
          {x : B}
          {f g h : x --> e}
          {α : f ==> g}
          {β : g ==> h}
          ( : is_cartesian_2cell_sfib p α)
          ( : is_cartesian_2cell_sfib p β).

  Definition vcomp_is_cartesian_2cell_sfib_unique
             {k : x --> e}
             {ζ : k ==> h}
             {δp : k · p ==> f · p}
             (q : ζ p = δp ((α β) p))
    : isaprop ( δ : k ==> f, δ p = δp × δ (α β) = ζ).
  Show proof.
    use invproofirrelevance.
    intros φ φ.
    use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ].
    rewrite <- rwhisker_vcomp in q.
    rewrite !vassocr in q.
    use (is_cartesian_2cell_sfib_factor_unique
           _
           
           _
           (is_cartesian_2cell_sfib_factor _ ζ (δp (α _)) q)
           δp
           (is_cartesian_2cell_sfib_factor_over _ _ _)
           _ _
           (pr12 φ)
           (pr12 φ)) ;
    use (is_cartesian_2cell_sfib_factor_unique
           _
           
           _
           ζ
           (δp (α _))
           q
           _
           _
           _
           (is_cartesian_2cell_sfib_factor_over _ _ _)
           _
           (is_cartesian_2cell_sfib_factor_comm _ _ _)).
    - rewrite <- rwhisker_vcomp.
      rewrite (pr12 φ).
      apply idpath.
    - rewrite !vassocl.
      apply (pr22 φ).
    - rewrite <- rwhisker_vcomp.
      rewrite (pr12 φ).
      apply idpath.
    - rewrite !vassocl.
      apply (pr22 φ).

  Definition vcomp_is_cartesian_2cell_sfib
    : is_cartesian_2cell_sfib p (α β).
  Show proof.
    intros k ζ δp q.
    use iscontraprop1.
    - apply vcomp_is_cartesian_2cell_sfib_unique.
      exact q.
    - simple refine (_ ,, _ ,, _).
      + simple refine (is_cartesian_2cell_sfib_factor _ _ δp _).
        * simple refine (is_cartesian_2cell_sfib_factor _ ζ (δp (α p)) _).
          abstract
            (rewrite !vassocl ;
             rewrite q ;
             rewrite <- rwhisker_vcomp ;
             apply idpath).
        * apply is_cartesian_2cell_sfib_factor_over.
      + apply is_cartesian_2cell_sfib_factor_over.
      + abstract
          (simpl ;
           rewrite !vassocr ;
           rewrite !is_cartesian_2cell_sfib_factor_comm ;
           apply idpath).
End VcompIsCartesian.

Definition invertible_is_cartesian_2cell_sfib
           {B : bicat}
           {e b : B}
           (p : e --> b)
           {x : B}
           {f g : x --> e}
           (α : f ==> g)
           ( : is_invertible_2cell α)
  : is_cartesian_2cell_sfib p α.
Show proof.
  intros h ζ δp q.
  use iscontraprop1.
  - abstract
      (use invproofirrelevance ;
       intros φ φ ;
       use subtypePath ;
         [ intro ; apply isapropdirprod ; apply cellset_property | ] ;
       refine (!(id2_right _) @ _ @ id2_right _) ;
       rewrite <- (vcomp_rinv ) ;
       rewrite !vassocr ;
       rewrite (pr22 φ), (pr22 φ) ;
       apply idpath).
  - refine (ζ ^-1 ,, _ ,, _).
    + abstract
        (rewrite <- rwhisker_vcomp ;
         use vcomp_move_R_Mp ; [ is_iso | ] ;
         cbn ;
         exact q).
    + abstract
        (rewrite !vassocl ;
         rewrite vcomp_linv ;
         apply id2_right).

Section PostComposition.
  Context {B : bicat}
          {e b : B}
          (p : e --> b)
          {x : B}
          {f g h : x --> e}
          (α : f ==> g) {β : g ==> h}
          {γ : f ==> h}
          ( : is_cartesian_2cell_sfib p β)
          ( : is_cartesian_2cell_sfib p γ)
          (q : α β = γ).

  Section PostCompositionFactor.
    Context {k : x --> e}
            {δ : k ==> g}
            (δp : k · p ==> f · p)
            (r : δ p = δp (α p)).

    Definition is_cartesian_2cell_sfib_postcomp_factor
      : k ==> f.
    Show proof.
      use (is_cartesian_2cell_sfib_factor _ (δ β) δp).
      abstract
        (rewrite <- rwhisker_vcomp ;
         rewrite r ;
         rewrite !vassocl ;
         rewrite rwhisker_vcomp ;
         rewrite q ;
         apply idpath).

    Definition is_cartesian_2cell_sfib_postcomp_comm
      : is_cartesian_2cell_sfib_postcomp_factor α = δ.
    Show proof.
      use (is_cartesian_2cell_sfib_factor_unique
             _
             
             k
             (δ β)
             (δ p)).
      - rewrite rwhisker_vcomp.
        apply idpath.
      - rewrite <- rwhisker_vcomp.
        etrans.
        {
          apply maponpaths_2.
          apply is_cartesian_2cell_sfib_factor_over.
        }
        rewrite r.
        apply idpath.
      - apply idpath.
      - rewrite !vassocl.
        etrans.
        {
          apply maponpaths.
          exact q.
        }
        apply is_cartesian_2cell_sfib_factor_comm.
      - apply idpath.

    Definition is_cartesian_2cell_sfib_postcomp_unique
      : isaprop ( φ, φ p = δp × φ α = δ).
    Show proof.
      use invproofirrelevance.
      intros φ φ.
      use subtypePath.
      {
        intro.
        apply isapropdirprod ; apply cellset_property.
      }
      use (is_cartesian_2cell_sfib_factor_unique
             _
             
             _
             (δ β)
             δp).
      - rewrite <- rwhisker_vcomp.
        rewrite r.
        rewrite !vassocl.
        rewrite rwhisker_vcomp.
        rewrite q.
        apply idpath.
      - exact (pr12 φ).
      - exact (pr12 φ).
      - rewrite <- q.
        rewrite !vassocr.
        apply maponpaths_2.
        exact (pr22 φ).
      - rewrite <- q.
        rewrite !vassocr.
        apply maponpaths_2.
        exact (pr22 φ).
  End PostCompositionFactor.

  Definition is_cartesian_2cell_sfib_postcomp
    : is_cartesian_2cell_sfib p α.
  Show proof.
    intros k δ δp r.
    use iscontraprop1.
    - exact (is_cartesian_2cell_sfib_postcomp_unique δp r).
    - simple refine (_ ,, _ ,, _).
      + exact (is_cartesian_2cell_sfib_postcomp_factor δp r).
      + apply is_cartesian_2cell_sfib_factor_over.
      + exact (is_cartesian_2cell_sfib_postcomp_comm δp r).
End PostComposition.

Definition is_cartesian_eq
           {B : bicat}
           {e b : B}
           {p : e --> b}
           {x : B}
           {f g : x --> e}
           (α : f ==> g)
           {β : f ==> g}
           (q : α = β)
           ( : is_cartesian_2cell_sfib p α)
  : is_cartesian_2cell_sfib p β.
Show proof.
  intros h ζ δp r.
  use iscontraprop1.
  - abstract
      (use invproofirrelevance ;
       intros φ φ ;
       use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ;
       induction q ;
       exact (is_cartesian_2cell_sfib_factor_unique
                _
                 h ζ δp
                r _ _
                (pr12 φ)
                (pr12 φ)
                (pr22 φ)
                (pr22 φ))).
  - simple refine (_ ,, _).
    + refine (is_cartesian_2cell_sfib_factor _ ζ δp _).
      abstract
        (rewrite q, r ;
         apply idpath).
    + split.
      * apply is_cartesian_2cell_sfib_factor_over.
      * abstract
          (refine (maponpaths (λ z, _ z) (!q) @ _) ;
           apply is_cartesian_2cell_sfib_factor_comm).

Definition is_cartesian_from_factor
           {B : bicat}
           {e b : B}
           {p : e --> b}
           {x : B}
           {f₁ f₂ g : x --> e}
           (α : f₁ ==> f₂)
           ( : is_invertible_2cell α)
           (β : f₁ ==> g)
           (γ : f₂ ==> g)
           ( : is_cartesian_2cell_sfib p γ)
           (q : β = α γ)
  : is_cartesian_2cell_sfib p β.
Show proof.
  use (is_cartesian_eq _ (!q)).
  use vcomp_is_cartesian_2cell_sfib.
  - apply invertible_is_cartesian_2cell_sfib.
    exact .
  - exact .

Definition map_between_cartesians
           {B : bicat}
           {x e b : B}
           {p : e --> b}
           {g₀ g₁ g₂ : x --> e}
           {α : g₀ ==> g₂}
           ( : is_cartesian_2cell_sfib p α)
           {β : g₁ ==> g₂}
           ( : is_cartesian_2cell_sfib p β)
           (δ : invertible_2cell (g₀ · p) (g₁ · p))
           (r : α p = δ (β p))
  : g₀ ==> g₁
  := is_cartesian_2cell_sfib_factor _ α δ r.

Section InvertibleBetweenCartesians.
  Context {B : bicat}
          {x e b : B}
          {p : e --> b}
          {g₀ g₁ g₂ : x --> e}
          {α : g₀ ==> g₂}
          ( : is_cartesian_2cell_sfib p α)
          {β : g₁ ==> g₂}
          ( : is_cartesian_2cell_sfib p β)
          (δ : invertible_2cell (g₀ · p) (g₁ · p))
          (r : α p = δ (β p)).

  Let φ : g₀ ==> g₁ := map_between_cartesians δ r.

  Local Lemma invertible_between_cartesians_help
    : β p = δ^-1 (α p).
  Show proof.
    cbn.
    use vcomp_move_L_pM ; is_iso ; cbn.
    exact (!r).

  Let ψ : g₁ ==> g₀
    := map_between_cartesians
         
         (inv_of_invertible_2cell δ)
         invertible_between_cartesians_help.

  Local Lemma invertible_between_cartesians_inv₁
    : φ ψ = id₂ _.
  Show proof.
    use (is_cartesian_2cell_sfib_factor_unique _ _ α (id2 _)).
    - rewrite id2_left.
      apply idpath.
    - unfold φ, ψ, map_between_cartesians.
      rewrite <- rwhisker_vcomp.
      rewrite !is_cartesian_2cell_sfib_factor_over.
      apply (vcomp_rinv δ).
    - apply id2_rwhisker.
    - unfold φ, ψ, map_between_cartesians.
      rewrite !vassocl.
      rewrite !is_cartesian_2cell_sfib_factor_comm.
      apply idpath.
    - apply id2_left.

  Local Lemma invertible_between_cartesians_inv₂
    : ψ φ = id₂ _.
  Show proof.
    use (is_cartesian_2cell_sfib_factor_unique _ _ β (id2 _)).
    - rewrite id2_left.
      apply idpath.
    - unfold φ, ψ, map_between_cartesians.
      rewrite <- rwhisker_vcomp.
      rewrite !is_cartesian_2cell_sfib_factor_over.
      apply (vcomp_linv δ).
    - apply id2_rwhisker.
    - unfold φ, ψ, map_between_cartesians.
      rewrite !vassocl.
      rewrite !is_cartesian_2cell_sfib_factor_comm.
      apply idpath.
    - apply id2_left.

  Definition invertible_between_cartesians
    : invertible_2cell g₀ g₁.
  Show proof.
    use make_invertible_2cell.
    - exact φ.
    - use make_is_invertible_2cell.
      + exact ψ.
      + exact invertible_between_cartesians_inv₁.
      + exact invertible_between_cartesians_inv₂.
End InvertibleBetweenCartesians.

3. Street fibrations in locally groupoidal bicategories
Definition locally_grpd_cartesian
           {B : bicat}
           (HB : locally_groupoid B)
           {e b : B}
           (p : e --> b)
           {x : B}
           {f g : x --> e}
           (γ : f ==> g)
  : is_cartesian_2cell_sfib p γ.
Show proof.
  intros h α δp q.
  pose (α_iso := make_invertible_2cell (HB _ _ _ _ α)).
  pose (γ_iso := make_invertible_2cell (HB _ _ _ _ γ)).
  use iscontraprop1.
  - abstract
      (use invproofirrelevance ;
       intros φ φ ;
       use subtypePath ;
       [ intro ; apply isapropdirprod ; apply cellset_property | ] ;
       use (vcomp_rcancel _ γ_iso) ;
       cbn ;
       exact (pr22 φ @ !(pr22 φ))).
  - refine (α γ_iso^-1 ,, _ ,, _).
    + abstract
        (rewrite <- rwhisker_vcomp ;
         use vcomp_move_R_Mp ; [ is_iso | ] ;
         cbn ;
         rewrite q ;
         apply idpath).
    + abstract
        (rewrite !vassocl ;
         rewrite vcomp_linv ;
         apply id2_right).

Definition locally_grpd_internal_sfib
           {B : bicat}
           (HB : locally_groupoid B)
           {e b : B}
           (p : e --> b)
  : internal_sfib p.
Show proof.
  split.
  - intros x f g α.
    refine (g
            ,,
            id2 _
            ,,
            inv_of_invertible_2cell (make_invertible_2cell (HB _ _ _ _ α))
            ,,
            locally_grpd_cartesian HB _ _
            ,,
            _).
    abstract
      (cbn ;
       rewrite id2_rwhisker ;
       rewrite vcomp_linv ;
       apply idpath).
  - intro ; intros.
    apply (locally_grpd_cartesian HB).

4. Morphisms of internal Street fibrations
Definition mor_preserves_cartesian
           {B : bicat}
           {e₁ b₁ : B}
           (p₁ : e₁ --> b₁)
           {e₂ b₂ : B}
           (p₂ : e₂ --> b₂)
           (fe : e₁ --> e₂)
  : UU
  := (x : B)
       (f g : x --> e₁)
       (γ : f ==> g)
       ( : is_cartesian_2cell_sfib p₁ γ),
     is_cartesian_2cell_sfib p₂ (γ fe).

Definition id_mor_preserves_cartesian
           {B : bicat}
           {e b : B}
           (p : e --> b)
  : mor_preserves_cartesian p p (id₁ e).
Show proof.
  intros ? ? ? ? H.
  assert (γ id₁ e = runitor _ γ rinvunitor _) as q.
  {
    use vcomp_move_L_Mp ; [ is_iso | ].
    cbn.
    rewrite !vcomp_runitor.
    apply idpath.
  }
  rewrite q.
  use vcomp_is_cartesian_2cell_sfib.
  - use vcomp_is_cartesian_2cell_sfib.
    + use invertible_is_cartesian_2cell_sfib.
      is_iso.
    + exact H.
  - use invertible_is_cartesian_2cell_sfib.
    is_iso.

Definition comp_preserves_cartesian
           {B : bicat}
           {e₁ b₁ e₂ b₂ e₃ b₃ : B}
           {p₁ : e₁ --> b₁}
           {p₂ : e₂ --> b₂}
           {p₃ : e₃ --> b₃}
           {fe₁ : e₁ --> e₂}
           {fe₂ : e₂ --> e₃}
           (H₁ : mor_preserves_cartesian p₁ p₂ fe₁)
           (H₂ : mor_preserves_cartesian p₂ p₃ fe₂)
  : mor_preserves_cartesian p₁ p₃ (fe₁ · fe₂).
Show proof.
  intros x f g γ .
  specialize (H₁ x _ _ γ ).
  specialize (H₂ x _ _ _ H₁).
  assert (γ fe₁ · fe₂
          =
          lassociator _ _ _
           ((γ fe₁) fe₂)
           rassociator _ _ _)
    as q.
  {
    use vcomp_move_L_Mp ; [ is_iso | ] ; cbn.
    rewrite rwhisker_rwhisker.
    apply idpath.
  }
  rewrite q.
  use vcomp_is_cartesian_2cell_sfib.
  - use vcomp_is_cartesian_2cell_sfib.
    + use invertible_is_cartesian_2cell_sfib.
      is_iso.
    + exact H₂.
  - use invertible_is_cartesian_2cell_sfib.
    is_iso.

Section Invertible2CellCartesian.
  Context {B : bicat}
          {x e b : B}
          {p p' : e --> b}
          (α : invertible_2cell p p')
          {f g : x --> e}
          {β : f ==> g}
          ( : is_cartesian_2cell_sfib p β)
          {k : x --> e}
          {ζ : k ==> g}
          (δp : k · p' ==> f · p')
          (q : ζ p' = δp (β p')).

  Let δp' : k · p ==> f · p
    := ((k α) δp (f α^-1)).

  Lemma help_eq
    : ζ p
      =
      (((k α) δp) (f α ^-1)) (β p).
  Show proof.
    rewrite !vassocl.
    use vcomp_move_L_pM.
    {
      is_iso.
      apply property_from_invertible_2cell.
    }
    cbn.
    rewrite <- vcomp_whisker.
    rewrite q.
    rewrite !vassocl.
    rewrite <- vcomp_whisker.
    apply idpath.

  Definition is_cartesian_2cell_sfib_factor_inv2cell_unique
    : isaprop ( (δ : k ==> f), δ p' = δp × δ β = ζ).
  Show proof.
    use invproofirrelevance.
    intros φ φ.
    use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ].
    use (is_cartesian_2cell_sfib_factor_unique
           _
           
           k ζ
           ((k α) δp (f α^-1))
           help_eq).
    - use vcomp_move_L_Mp ; [ is_iso | ].
      cbn.
      rewrite vcomp_whisker.
      apply maponpaths.
      exact (pr12 φ).
    - use vcomp_move_L_Mp ; [ is_iso | ].
      cbn.
      rewrite vcomp_whisker.
      apply maponpaths.
      exact (pr12 φ).
    - exact (pr22 φ).
    - exact (pr22 φ).

  Definition is_cartesian_2cell_sfib_factor_inv2cell
    : k ==> f
    := is_cartesian_2cell_sfib_factor
         _
         ζ
         ((k α) δp (f α^-1))
         help_eq.

  Definition is_cartesian_2cell_sfib_factor_inv2cell_over
    : is_cartesian_2cell_sfib_factor_inv2cell p' = δp.
  Show proof.
    use (vcomp_lcancel (_ α)).
    {
      is_iso.
      apply property_from_invertible_2cell.
    }
    rewrite <- vcomp_whisker.
    unfold is_cartesian_2cell_sfib_factor_inv2cell.
    rewrite is_cartesian_2cell_sfib_factor_over.
    rewrite !vassocl.
    rewrite lwhisker_vcomp.
    rewrite vcomp_linv.
    rewrite lwhisker_id2.
    rewrite id2_right.
    apply idpath.
End Invertible2CellCartesian.

Definition is_cartesian_2cell_sfib_inv2cell
           {B : bicat}
           {x e b : B}
           {p p' : e --> b}
           (α : invertible_2cell p p')
           {f g : x --> e}
           {β : f ==> g}
           ( : is_cartesian_2cell_sfib p β)
  : is_cartesian_2cell_sfib p' β.
Show proof.
  intros k ζ δp q.
  use iscontraprop1.
  - exact (is_cartesian_2cell_sfib_factor_inv2cell_unique α δp q).
  - simple refine (_ ,, _ ,, _).
    + exact (is_cartesian_2cell_sfib_factor_inv2cell α δp q).
    + exact (is_cartesian_2cell_sfib_factor_inv2cell_over α δp q).
    + apply is_cartesian_2cell_sfib_factor_comm.

Definition invertible_2cell_mor_between_preserves_cartesian
           {B : bicat}
           {e₁ e₂ b₁ b₂ : B}
           {p₁ : e₁ --> b₁}
           {p₂ : e₂ --> b₂}
           {fe fe' : e₁ --> e₂}
           (α : invertible_2cell fe fe')
           (H : mor_preserves_cartesian p₁ p₂ fe)
  : mor_preserves_cartesian p₁ p₂ fe'.
Show proof.
  intros x f g γ .
  assert (γ fe' (_ α^-1) = (f α^-1) (γ fe)) as p.
  {
    rewrite vcomp_whisker.
    apply idpath.
  }
  use (is_cartesian_2cell_sfib_postcomp _ _ _ _ p).
  - use invertible_is_cartesian_2cell_sfib.
    is_iso.
  - use vcomp_is_cartesian_2cell_sfib.
    + use invertible_is_cartesian_2cell_sfib.
      is_iso.
    + exact (H x f g γ ).

Definition invertible_2cell_between_preserves_cartesian
           {B : bicat}
           {e₁ e₂ b₁ b₂ : B}
           {p₁ p₁' : e₁ --> b₁}
           {p₂ p₂' : e₂ --> b₂}
           {fe fe' : e₁ --> e₂}
           (α : invertible_2cell p₁ p₁')
           (β : invertible_2cell p₂ p₂')
           (γ : invertible_2cell fe fe')
           (H : mor_preserves_cartesian p₁ p₂ fe)
  : mor_preserves_cartesian p₁' p₂' fe'.
Show proof.
  intros w h₁ h₂ ζ .
  use (is_cartesian_2cell_sfib_inv2cell β).
  use (invertible_2cell_mor_between_preserves_cartesian γ H).
  use (is_cartesian_2cell_sfib_inv2cell (inv_of_invertible_2cell α)).
  exact .

Definition locally_grpd_preserves_cartesian
           {B : bicat}
           (HB : locally_groupoid B)
           {e₁ b₁ e₂ b₂ : B}
           (p₁ : e₁ --> b₁)
           (p₂ : e₂ --> b₂)
           (fe : e₁ --> e₂)
  : mor_preserves_cartesian p₁ p₂ fe.
Show proof.
  intro ; intros.
  apply (locally_grpd_cartesian HB).

Definition isaprop_mor_preserves_cartesian
           {B : bicat}
           {e₁ b₁ : B}
           (p₁ : e₁ --> b₁)
           {e₂ b₂ : B}
           (p₂ : e₂ --> b₂)
           (fe : e₁ --> e₂)
  : isaprop (mor_preserves_cartesian p₁ p₂ fe).
Show proof.
  do 5 (use impred ; intro).
  exact (isaprop_is_cartesian_2cell_sfib _ _).

Definition mor_of_internal_sfib_over
           {B : bicat}
           {e₁ b₁ : B}
           (p₁ : e₁ --> b₁)
           {e₂ b₂ : B}
           (p₂ : e₂ --> b₂)
           (fb : b₁ --> b₂)
  : UU
  := (fe : e₁ --> e₂),
     mor_preserves_cartesian p₁ p₂ fe
     ×
     invertible_2cell (p₁ · fb) (fe · p₂).

Definition make_mor_of_internal_sfib_over
           {B : bicat}
           {e₁ b₁ : B}
           {p₁ : e₁ --> b₁}
           {e₂ b₂ : B}
           {p₂ : e₂ --> b₂}
           {fb : b₁ --> b₂}
           (fe : e₁ --> e₂)
           (fc : mor_preserves_cartesian p₁ p₂ fe)
           (f_com : invertible_2cell (p₁ · fb) (fe · p₂))
  : mor_of_internal_sfib_over p₁ p₂ fb
  := (fe ,, fc ,, f_com).

Coercion mor_of_internal_sfib_over_to_mor
         {B : bicat}
         {e₁ b₁ : B}
         {p₁ : e₁ --> b₁}
         {e₂ b₂ : B}
         {p₂ : e₂ --> b₂}
         {fb : b₁ --> b₂}
         (fe : mor_of_internal_sfib_over p₁ p₂ fb)
  : e₁ --> e₂
  := pr1 fe.

Definition mor_of_internal_sfib_over_preserves
           {B : bicat}
           {e₁ b₁ : B}
           {p₁ : e₁ --> b₁}
           {e₂ b₂ : B}
           {p₂ : e₂ --> b₂}
           {fb : b₁ --> b₂}
           (fe : mor_of_internal_sfib_over p₁ p₂ fb)
  : mor_preserves_cartesian p₁ p₂ fe
  := pr12 fe.

Definition mor_of_internal_sfib_over_com
           {B : bicat}
           {e₁ b₁ : B}
           {p₁ : e₁ --> b₁}
           {e₂ b₂ : B}
           {p₂ : e₂ --> b₂}
           {fb : b₁ --> b₂}
           (fe : mor_of_internal_sfib_over p₁ p₂ fb)
  : invertible_2cell (p₁ · fb) (fe · p₂)
  := pr22 fe.

Definition id_mor_of_internal_sfib_over
           {B : bicat}
           {e b : B}
           (p : e --> b)
  : mor_of_internal_sfib_over p p (id₁ _).
Show proof.
  use make_mor_of_internal_sfib_over.
  - exact (id₁ e).
  - apply id_mor_preserves_cartesian.
  - use make_invertible_2cell.
    + refine (runitor _ linvunitor _).
    + is_iso.

Definition comp_mor_of_internal_sfib_over
           {B : bicat}
           {e₁ e₂ e₃ b₁ b₂ b₃ : B}
           {fb₁ : b₁ --> b₂}
           {fb₂ : b₂ --> b₃}
           {p₁ : e₁ --> b₁}
           {p₂ : e₂ --> b₂}
           {p₃ : e₃ --> b₃}
           (fe₁ : mor_of_internal_sfib_over p₁ p₂ fb₁)
           (fe₂ : mor_of_internal_sfib_over p₂ p₃ fb₂)
  : mor_of_internal_sfib_over p₁ p₃ (fb₁ · fb₂).
Show proof.
  use make_mor_of_internal_sfib_over.
  - exact (fe₁ · fe₂).
  - exact (comp_preserves_cartesian
             (mor_of_internal_sfib_over_preserves fe₁)
             (mor_of_internal_sfib_over_preserves fe₂)).
  - use make_invertible_2cell.
    + exact (lassociator _ _ _
              (mor_of_internal_sfib_over_com fe₁ _)
              rassociator _ _ _
              (_ mor_of_internal_sfib_over_com fe₂)
              lassociator _ _ _).
    + is_iso.
      * apply property_from_invertible_2cell.
      * apply property_from_invertible_2cell.

5. Cells of internal Street fibrations
Definition cell_of_internal_sfib_over_homot
           {B : bicat}
           {b₁ b₂ e₁ e₂ : B}
           {fb gb : b₁ --> b₂}
           (γ : fb ==> gb)
           {p₁ : e₁ --> b₁}
           {p₂ : e₂ --> b₂}
           {fe : mor_of_internal_sfib_over p₁ p₂ fb}
           {ge : mor_of_internal_sfib_over p₁ p₂ gb}
           (γe : fe ==> ge)
  : UU
  := mor_of_internal_sfib_over_com fe (γe _)
     =
     (_ γ) mor_of_internal_sfib_over_com ge.

Definition cell_of_internal_sfib_over
           {B : bicat}
           {b₁ b₂ e₁ e₂ : B}
           {fb gb : b₁ --> b₂}
           (γ : fb ==> gb)
           {p₁ : e₁ --> b₁}
           {p₂ : e₂ --> b₂}
           (fe : mor_of_internal_sfib_over p₁ p₂ fb)
           (ge : mor_of_internal_sfib_over p₁ p₂ gb)
  : UU
  := (γe : fe ==> ge), cell_of_internal_sfib_over_homot γ γe.

Definition make_cell_of_internal_sfib_over
           {B : bicat}
           {b₁ b₂ e₁ e₂ : B}
           {fb gb : b₁ --> b₂}
           {γ : fb ==> gb}
           {p₁ : e₁ --> b₁}
           {p₂ : e₂ --> b₂}
           {fe : mor_of_internal_sfib_over p₁ p₂ fb}
           {ge : mor_of_internal_sfib_over p₁ p₂ gb}
           (γe : fe ==> ge)
           (p : cell_of_internal_sfib_over_homot γ γe)
  : cell_of_internal_sfib_over γ fe ge
  := (γe ,, p).

Coercion cell_of_cell_of_internal_sfib_over
         {B : bicat}
         {b₁ b₂ e₁ e₂ : B}
         {fb gb : b₁ --> b₂}
         {γ : fb ==> gb}
         {p₁ : e₁ --> b₁}
         {p₂ : e₂ --> b₂}
         {fe : mor_of_internal_sfib_over p₁ p₂ fb}
         {ge : mor_of_internal_sfib_over p₁ p₂ gb}
         (γe : cell_of_internal_sfib_over γ fe ge)
  : fe ==> ge
  := pr1 γe.

Definition cell_of_internal_sfib_over_eq
           {B : bicat}
           {b₁ b₂ e₁ e₂ : B}
           {fb gb : b₁ --> b₂}
           {γ : fb ==> gb}
           {p₁ : e₁ --> b₁}
           {p₂ : e₂ --> b₂}
           {fe : mor_of_internal_sfib_over p₁ p₂ fb}
           {ge : mor_of_internal_sfib_over p₁ p₂ gb}
           (γe : cell_of_internal_sfib_over γ fe ge)
  : mor_of_internal_sfib_over_com fe (γe _)
     =
     (_ γ) mor_of_internal_sfib_over_com ge
  := pr2 γe.

Definition eq_cell_of_internal_sfib_over
           {B : bicat}
           {b₁ b₂ e₁ e₂ : B}
           {fb gb : b₁ --> b₂}
           {γ : fb ==> gb}
           {p₁ : e₁ --> b₁}
           {p₂ : e₂ --> b₂}
           {fe : mor_of_internal_sfib_over p₁ p₂ fb}
           {ge : mor_of_internal_sfib_over p₁ p₂ gb}
           (γe₁ γe₂ : cell_of_internal_sfib_over γ fe ge)
           (p : pr1 γe₁ = γe₂)
  : γe₁ = γe₂.
Show proof.
  use subtypePath.
  {
    intro.
    apply cellset_property.
  }
  exact p.