Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.
Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat.
Require Import UniMath.Bicategories.DisplayedBicats.FiberCategory.
Require Import UniMath.Bicategories.DisplayedBicats.FiberBicategory.FiberBicategory1.

Local Open Scope cat.
Local Open Scope mor_disp_scope.

Section LocalIsoFibration.
  Context {C : bicat}.

  Variable (D : disp_bicat C) (h : local_iso_cleaving D) (c : C).

  Local Arguments transportf {_} {_} {_} {_} {_} _.
  Local Arguments transportb {_} {_} {_} {_} {_} _.
  Local Arguments disp_lassociator {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}.
  Local Arguments disp_rassociator {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}.
  Local Notation "'ℓ1'" := (local_iso_cleaving_1cell h _ (idempunitor c))
                             (at level 0).
  Local Notation "'ℓ2'" := (disp_local_iso_cleaving_invertible_2cell h _ (idempunitor c))
                             (at level 0).
  Local Notation "f ^-1" := (disp_inv_cell f).

  Definition strict_fiber_bicat_data_laws_rassociator_lassociator
    : ∏ (a₁ a₂ a₃ a₄ : strict_fiber_bicat_data D h c)
         (f₁ : strict_fiber_bicat_data D h c ⟦ a₁ , a₂ ⟧)
         (f₂ : strict_fiber_bicat_data D h c ⟦ a₂ , a₃ ⟧)
         (f₃ : strict_fiber_bicat_data D h c ⟦ a₃ , a₄ ⟧),
       rassociator f₁ f₂ f₃ • lassociator f₁ f₂ f₃
       =
       id₂ (f₁ · f₂ · f₃).
  Show proof.

  Definition strict_fiber_bicat_data_laws_runitor_rwhisker
    : ∏ (a₁ a₂ a₃ : strict_fiber_bicat_data D h c)
        (f : strict_fiber_bicat_data D h c ⟦ a₁ , a₂ ⟧)
        (g : strict_fiber_bicat_data D h c ⟦ a₂ , a₃ ⟧),
      lassociator f (id₁ a₂) g • (runitor f ▹ g)
      =
      f ◃ lunitor g.
  Show proof.

  Section LassociatorLassociator.
    Variable (a₁ a₂ a₃ a₄ a₅ : strict_fiber_bicat_data D h c)
             (f₁ : strict_fiber_bicat_data D h c ⟦ a₁ , a₂ ⟧)
             (f₂ : strict_fiber_bicat_data D h c ⟦ a₂ , a₃ ⟧)
             (f₃ : strict_fiber_bicat_data D h c ⟦ a₃ , a₄ ⟧)
             (f₄ : strict_fiber_bicat_data D h c ⟦ a₄ , a₅ ⟧).
    Arguments transportf {_} _ {_} {_} _ _.

    Local Definition step1
      : ∑ p,
        ((f₁ ◃ lassociator f₂ f₃ f₄)
           • lassociator f₁ (f₂ · f₃) f₄)
          • (lassociator f₁ f₂ f₃ ▹ f₄)
        =
        transportf
          (λ z, _ ==>[ z] _)
          p
          ((((ℓ2 •• (f₁ ◃◃ (((ℓ2 •• (f₂ ◃◃ ℓ2)) •• disp_lassociator)
                              •• ((ℓ2 ^-1 ▹▹ f₄) •• ℓ2 ^-1)))) •• ℓ2 ^-1)
              •• (((ℓ2 •• (f₁ ◃◃ ℓ2)) •• disp_lassociator)
                    •• ((ℓ2 ^-1 ▹▹ f₄) •• ℓ2^-1)))
             •• ((ℓ2 •• ((((ℓ2 •• (f₁ ◃◃ ℓ2)) •• disp_lassociator)
                            •• ((ℓ2^-1 ▹▹ f₃) •• ℓ2^-1)) ▹▹ f₄)) •• ℓ2^-1)).
    Show proof.

    Local Definition step2
      : ∑ p,
        transportf
          (λ z, _ ==>[ z] _)
          p
          ((((ℓ2 •• (f₁ ◃◃ ℓ2)) •• disp_lassociator)
              •• ((ℓ2 ^-1 ▹▹ ℓ1) •• ℓ2^-1))
             •• (((ℓ2 •• (ℓ1 ◃◃ ℓ2)) •• disp_lassociator)
                   •• ((ℓ2^-1 ▹▹ f₄) •• ℓ2^-1)))
        =
        lassociator f₁ f₂ (f₃ · f₄) • lassociator (f₁ · f₂) f₃ f₄.
    Show proof.

    Local Definition step3
      : ∑ p,
        transportf
          (λ z, _ ==>[ z] _)
          (pr1 step1)
          ((((ℓ2 •• (f₁ ◃◃ (((ℓ2 •• (f₂ ◃◃ ℓ2)) •• disp_lassociator)
                              •• ((ℓ2 ^-1 ▹▹ f₄) •• ℓ2 ^-1)))) •• ℓ2 ^-1)
              •• (((ℓ2 •• (f₁ ◃◃ ℓ2)) •• disp_lassociator)
                    •• ((ℓ2 ^-1 ▹▹ f₄) •• ℓ2^-1)))
             •• ((ℓ2 •• ((((ℓ2 •• (f₁ ◃◃ ℓ2)) •• disp_lassociator)
                            •• ((ℓ2^-1 ▹▹ f₃) •• ℓ2^-1)) ▹▹ f₄)) •• ℓ2^-1))
        =
        transportf
          (λ z, _ ==>[ z ] _)
          p
          ((ℓ2 •• (f₁ ◃◃ (((ℓ2 •• (f₂ ◃◃ ℓ2)) •• disp_lassociator)
                            •• ((ℓ2 ^-1 ▹▹ f₄) •• ℓ2^-1))))
             •• ((((f₁ ◃◃ ℓ2) •• disp_lassociator)
                    •• ((ℓ2^-1 ▹▹ f₄) •• ℓ2^-1))
                   •• ((ℓ2 •• ((((ℓ2 •• (f₁ ◃◃ ℓ2)) •• disp_lassociator)
                                  •• ((ℓ2^-1 ▹▹ f₃) •• ℓ2^-1)) ▹▹ f₄))
                         •• ℓ2^-1))).
    Show proof.

    Local Definition step4
      : ∑ p,
        transportf
          (λ z, _ ==>[ z ] _)
          (pr1 step3)
          ((ℓ2 •• (f₁ ◃◃ (((ℓ2 •• (f₂ ◃◃ ℓ2)) •• disp_lassociator)
                            •• ((ℓ2 ^-1 ▹▹ f₄) •• ℓ2^-1))))
             •• ((((f₁ ◃◃ ℓ2) •• disp_lassociator)
                    •• ((ℓ2^-1 ▹▹ f₄) •• ℓ2^-1))
                   •• ((ℓ2 •• ((((ℓ2 •• (f₁ ◃◃ ℓ2)) •• disp_lassociator)
                                  •• ((ℓ2^-1 ▹▹ f₃) •• ℓ2^-1)) ▹▹ f₄))
                         •• ℓ2^-1)))
        =
        transportf
          (λ z, _ ==>[ z] _)
          p
          ((ℓ2 •• (f₁ ◃◃ (((ℓ2 •• (f₂ ◃◃ ℓ2)) •• disp_lassociator)
                            •• ((ℓ2^-1 ▹▹ f₄) •• ℓ2^-1))))
             •• (((f₁ ◃◃ ℓ2) •• disp_lassociator)
                   •• ((ℓ2^-1 ▹▹ f₄)
                         •• (((((ℓ2 •• (f₁ ◃◃ ℓ2)) •• disp_lassociator)
                                 •• ((ℓ2^-1 ▹▹ f₃) •• ℓ2^-1)) ▹▹ f₄)
                               •• ℓ2^-1)))).
    Show proof.

    Local Definition step5
      : ∑ p,
        transportf
          (λ z, _ ==>[ z] _)
          (pr1 step4)
          ((ℓ2 •• (f₁ ◃◃ (((ℓ2 •• (f₂ ◃◃ ℓ2)) •• disp_lassociator)
                            •• ((ℓ2^-1 ▹▹ f₄) •• ℓ2^-1))))
             •• (((f₁ ◃◃ ℓ2) •• disp_lassociator)
                   •• ((ℓ2^-1 ▹▹ f₄)
                         •• (((((ℓ2 •• (f₁ ◃◃ ℓ2)) •• disp_lassociator)
                                 •• ((ℓ2^-1 ▹▹ f₃) •• ℓ2^-1)) ▹▹ f₄)
                               •• ℓ2^-1))))
        =
        transportf
          (λ z, _ ==>[ z] _)
          p
          ((ℓ2 •• ((f₁ ◃◃ ℓ2)
                     •• (f₁ ◃◃ ((f₂ ◃◃ ℓ2)
                                  •• (disp_lassociator
                                        •• ((ℓ2^-1 ▹▹ f₄)
                                              •• ℓ2^-1))))))
             •• (((f₁ ◃◃ ℓ2) •• disp_lassociator)
                   •• ((ℓ2^-1 ▹▹ f₄)
                         •• (((((ℓ2 •• (f₁ ◃◃ ℓ2))
                                  •• disp_lassociator)
                                 •• ((ℓ2^-1 ▹▹ f₃)
                                       •• ℓ2^-1)) ▹▹ f₄)
                               •• ℓ2^-1)))).
    Show proof.

    Local Definition step6
      : ∑ p,
        transportf
          (λ z, _ ==>[ z] _)
          (pr1 step5)
          ((ℓ2 •• ((f₁ ◃◃ ℓ2)
                     •• (f₁ ◃◃ ((f₂ ◃◃ ℓ2)
                                  •• (disp_lassociator
                                        •• ((ℓ2^-1 ▹▹ f₄)
                                              •• ℓ2^-1))))))
             •• (((f₁ ◃◃ ℓ2) •• disp_lassociator)
                   •• ((ℓ2^-1 ▹▹ f₄)
                         •• (((((ℓ2 •• (f₁ ◃◃ ℓ2))
                                  •• disp_lassociator)
                                 •• ((ℓ2^-1 ▹▹ f₃)
                                       •• ℓ2^-1)) ▹▹ f₄)
                               •• ℓ2^-1))))
        =
        transportf
          (λ z, _ ==>[ z] _)
          p
          (ℓ2 •• ((f₁ ◃◃ ℓ2)
                    •• (((f₁ ◃◃ ((f₂ ◃◃ ℓ2)
                                   •• (disp_lassociator
                                         •• (ℓ2^-1 ▹▹ f₄))))
                           •• disp_lassociator)
                          •• ((ℓ2^-1 ▹▹ f₄)
                                •• (((((ℓ2
                                          •• (f₁ ◃◃ ℓ2))
                                         •• disp_lassociator)
                                        •• ((ℓ2^-1 ▹▹ f₃)
                                              •• ℓ2^-1)) ▹▹ f₄)
                                      •• ℓ2^-1))))).
    Show proof.

    Local Definition step7
      : ∑ p,
        transportf
          (λ z, _ ==>[ z] _)
          (pr1 step6)
          (ℓ2 •• ((f₁ ◃◃ ℓ2)
                    •• (((f₁ ◃◃ ((f₂ ◃◃ ℓ2)
                                   •• (disp_lassociator
                                         •• (ℓ2^-1 ▹▹ f₄))))
                           •• disp_lassociator)
                          •• ((ℓ2^-1 ▹▹ f₄)
                                •• (((((ℓ2
                                          •• (f₁ ◃◃ ℓ2))
                                         •• disp_lassociator)
                                        •• ((ℓ2^-1 ▹▹ f₃)
                                              •• ℓ2^-1)) ▹▹ f₄)
                                      •• ℓ2^-1)))))
        =
        transportf
          (λ z, _ ==>[ z] _)
          p
          (ℓ2 •• ((f₁ ◃◃ ℓ2)
                    •• (((f₁ ◃◃ ((f₂ ◃◃ ℓ2)
                                   •• disp_lassociator))
                           •• (disp_lassociator
                                 •• ((f₁ ◃◃ ℓ2^-1) ▹▹ f₄)))
                          •• ((ℓ2^-1 ▹▹ f₄)
                                •• (((((ℓ2 •• (f₁ ◃◃ ℓ2))
                                         •• disp_lassociator)
                                        •• ((ℓ2^-1 ▹▹ f₃)
                                              •• ℓ2^-1)) ▹▹ f₄)
                                      •• ℓ2^-1))))).
    Show proof.

    Local Definition step8
      : ∑ p,
        transportf
          (λ z, _ ==>[ z] _)
          (pr1 step7)
          (ℓ2 •• ((f₁ ◃◃ ℓ2)
                    •• (((f₁ ◃◃ ((f₂ ◃◃ ℓ2)
                                   •• disp_lassociator))
                           •• (disp_lassociator
                                 •• ((f₁ ◃◃ ℓ2^-1) ▹▹ f₄)))
                          •• ((ℓ2^-1 ▹▹ f₄)
                                •• (((((ℓ2 •• (f₁ ◃◃ ℓ2))
                                         •• disp_lassociator)
                                        •• ((ℓ2^-1 ▹▹ f₃)
                                              •• ℓ2^-1)) ▹▹ f₄)
                                      •• ℓ2^-1)))))
        =
        transportf (λ z, _ ==>[ z] _)
                   p
                   (ℓ2
                      •• ((f₁ ◃◃ ℓ2)
                            •• (((f₁ ◃◃ ((f₂ ◃◃ ℓ2)
                                           •• disp_lassociator))
                                   •• (disp_lassociator
                                         •• ((f₁ ◃◃ ℓ2 ^-1) ▹▹ f₄)))
                                  •• ((((((f₁ ◃◃ ℓ2)
                                            •• disp_lassociator)
                                           •• (ℓ2 ^-1 ▹▹ f₃))
                                          •• ℓ2 ^-1) ▹▹ f₄)
                                        •• ℓ2 ^-1)))).
    Show proof.

    Local Definition step9
      : ∑ p,
        transportf
          (λ z, _ ==>[ z] _)
          (pr1 step8)
          (ℓ2
             •• ((f₁ ◃◃ ℓ2)
                   •• (((f₁ ◃◃ ((f₂ ◃◃ ℓ2)
                                  •• disp_lassociator))
                          •• (disp_lassociator
                                •• ((f₁ ◃◃ ℓ2 ^-1) ▹▹ f₄)))
                         •• ((((((f₁ ◃◃ ℓ2)
                                   •• disp_lassociator)
                                  •• (ℓ2 ^-1 ▹▹ f₃))
                                 •• ℓ2 ^-1) ▹▹ f₄)
                               •• ℓ2 ^-1))))
        =
        transportf
          (λ z, _ ==>[ z] _)
          p
          (ℓ2
             •• ((f₁ ◃◃ ℓ2)
                   •• ((f₁ ◃◃ ((f₂ ◃◃ ℓ2) •• disp_lassociator))
                         •• (disp_lassociator
                               •• ((((disp_lassociator
                                        •• (ℓ2 ^-1 ▹▹ f₃))
                                       •• ℓ2 ^-1) ▹▹ f₄)
                                     •• ℓ2 ^-1))))).
    Show proof.

    Local Definition step10
      : ∑ p,
        transportf
          (λ z, _ ==>[ z] _)
          (pr1 step9)
          (ℓ2
             •• ((f₁ ◃◃ ℓ2)
                   •• ((f₁ ◃◃ ((f₂ ◃◃ ℓ2) •• disp_lassociator))
                         •• (disp_lassociator
                               •• ((((disp_lassociator
                                        •• (ℓ2 ^-1 ▹▹ f₃))
                                       •• ℓ2 ^-1) ▹▹ f₄)
                                     •• ℓ2 ^-1)))))
        =
        transportf
          (λ z, _ ==>[ z] _)
          p
          (ℓ2
             •• ((f₁ ◃◃ ℓ2)
                   •• ((f₁ ◃◃ (f₂ ◃◃ ℓ2))
                         •• (((disp_lassociator •• disp_lassociator)
                                •• (((ℓ2 ^-1 ▹▹ f₃) •• ℓ2 ^-1) ▹▹ f₄))
                               •• ℓ2 ^-1)))).
    Show proof.

    Local Definition step11
      : ∑ p,
        transportf
          (λ z, _ ==>[ z] _)
          (pr1 step10)
          (ℓ2
             •• ((f₁ ◃◃ ℓ2)
                   •• ((f₁ ◃◃ (f₂ ◃◃ ℓ2))
                         •• (((disp_lassociator •• disp_lassociator)
                                •• (((ℓ2 ^-1 ▹▹ f₃) •• ℓ2 ^-1) ▹▹ f₄))
                               •• ℓ2 ^-1))))
        =
        transportf
          (λ z, _ ==>[ z] _)
          p
          (ℓ2
             •• ((f₁ ◃◃ ℓ2)
                   •• ((((disp_lassociator •• (f₁;; f₂ ◃◃ ℓ2)) •• disp_lassociator)
                          •• (((ℓ2 ^-1 ▹▹ f₃) •• ℓ2 ^-1) ▹▹ f₄)) •• ℓ2 ^-1))).
    Show proof.

    Local Definition step12
      : ∑ p,
        transportf
          (λ z, _ ==>[ z] _)
          (pr1 step11)
          (ℓ2
             •• ((f₁ ◃◃ ℓ2)
                   •• ((((disp_lassociator •• (f₁;; f₂ ◃◃ ℓ2)) •• disp_lassociator)
                          •• (((ℓ2 ^-1 ▹▹ f₃) •• ℓ2 ^-1) ▹▹ f₄)) •• ℓ2 ^-1)))
        =
        transportf
          (λ z, _ ==>[ z] _)
          p
          (ℓ2
             •• ((f₁ ◃◃ ℓ2)
                   •• (((disp_lassociator •• (f₁;; f₂ ◃◃ ℓ2))
                          •• (((ℓ2 ^-1 ▹▹ f₃;; f₄)
                                 •• disp_lassociator)
                                •• (ℓ2 ^-1 ▹▹ f₄)))
                         •• ℓ2 ^-1))).
    Show proof.

    Local Definition step13
      : ∑ p,
        transportf
          (λ z, _ ==>[ z] _)
          (pr1 step12)
          (ℓ2
             •• ((f₁ ◃◃ ℓ2)
                   •• (((disp_lassociator •• (f₁;; f₂ ◃◃ ℓ2))
                          •• (((ℓ2 ^-1 ▹▹ f₃;; f₄)
                                 •• disp_lassociator)
                                •• (ℓ2 ^-1 ▹▹ f₄)))
                         •• ℓ2 ^-1)))
        =
        transportf
          (λ z, _ ==>[ z] _)
          p
          (ℓ2
             •• ((f₁ ◃◃ ℓ2)
                   •• (((disp_lassociator •• (((ℓ2 ^-1 ▹▹ ℓ1) •• (ℓ1 ◃◃ ℓ2))
                                                •• disp_lassociator))
                          •• (ℓ2 ^-1 ▹▹ f₄))
                         •• ℓ2 ^-1))).
    Show proof.

    Local Arguments transportf {_} _ {_} {_} {_} _.

    Definition strict_fiber_bicat_data_laws_lassociator_lassociator
      : ((f₁ ◃ lassociator f₂ f₃ f₄)
           • lassociator f₁ (f₂ · f₃) f₄)
          • (lassociator f₁ f₂ f₃ ▹ f₄)
        =
        lassociator f₁ f₂ (f₃ · f₄) • lassociator (f₁ · f₂) f₃ f₄.
    Show proof.
  End LassociatorLassociator.

  Definition strict_fiber_bicat_data_laws : prebicat_laws (strict_fiber_bicat_data D h c).
  Show proof.

  Definition strict_fiber_prebicat : prebicat.
  Show proof.

  Definition strict_fiber_bicat : bicat.
  Show proof.
End LocalIsoFibration.

Definition strict_fiber_bicat_invertible_2cell
           {B : bicat}
           {D : disp_bicat B}
           {HD : local_iso_cleaving D}
           {b : B}
           {x y : strict_fiber_bicat D HD b}
           {f g : x --> y}
           {α : f ==> g}
           (Hα : is_disp_invertible_2cell (id2_invertible_2cell _) α)
  : is_invertible_2cell α.
Show proof.