Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat.
Require Import UniMath.Bicategories.PseudoFunctors.Display.Base.
Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells.
Require Import UniMath.Bicategories.PseudoFunctors.Display.Map2Cells.
Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictIdentitor.
Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictCompositor.
Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictPseudoFunctorBicat.

Local Open Scope bicategory_scope.
Local Open Scope cat.

Definition strict_psfunctor
           (C D : bicat)
  : UU
  := strict_psfunctor_bicat C D.

Definition make_strict_psfunctor_data
           {C D : bicat}
           (F₀ : C → D)
           (F₁ : ∏ {a b : C}, C⟦a,b⟧ → D⟦F₀ a, F₀ b⟧)
           (F₂ : ∏ {a b : C} {f g : C⟦a,b⟧}, f ==> g → F₁ f ==> F₁ g)
           (Fid : ∏ (a : C), identity (F₀ a) = F₁ (identity a))
           (Fcomp : (∏ (a b c : C) (f : a --> b) (g : b --> c),
                     F₁ f · F₁ g = F₁ (f · g)))
  : strict_psfunctor_data C D.
Proof.
  exact ((F₀ ,, F₁) ,, (F₂ ,, Fid ,, Fcomp)).
Defined.

Definition make_strict_psfunctor
           {C D : bicat}
           (F : strict_psfunctor_data C D)
           (HF : is_strict_psfunctor F)
  : strict_psfunctor C D
  := (F ,, HF).

Coercion strict_psfunctor_to_strict_psfunctor_data
         {C D : bicat}
         (F : strict_psfunctor C D)
  : strict_psfunctor_data C D
  := pr1 F.

Definition strict_psfunctor_on_cells
           {C D : bicat}
           (F : strict_psfunctor C D)
           {a b : C}
           {f g : a --> b}
           (x : f ==> g)
  : #F f ==> #F g
  := pr12 (pr1 F) a b f g x.

Definition strict_psfunctor_id
           {C D : bicat}
           (F : strict_psfunctor C D)
           (a : C)
  : identity (F a) = #F (identity a)
  := pr1 (pr221 F) a.

Definition strict_psfunctor_comp
           {C D : bicat}
           (F : strict_psfunctor C D)
           {a b c : C}
           (f : a --> b)
           (g : b --> c)
  : #F f · #F g = #F (f · g)
  := pr2 (pr221 F) _ _ _ f g.

Definition strict_psfunctor_id_cell
           {C D : bicat}
           (F : strict_psfunctor C D)
           (a : C)
  : invertible_2cell (identity (F a)) (#F (identity a))
  := idtoiso_2_1 _ _ (strict_psfunctor_id F a).

Definition strict_psfunctor_comp_cell
           {C D : bicat}
           (F : strict_psfunctor C D)
           {a b c : C}
           (f : a --> b)
           (g : b --> c)
  : invertible_2cell (#F f · #F g) (#F (f · g))
  := idtoiso_2_1 _ _ (strict_psfunctor_comp F f g).

Local Notation "'##'" := (strict_psfunctor_on_cells).

Section StrictProjection.
  Context {C D : bicat}.
  Variable (F : strict_psfunctor C D).

  Definition strict_psfunctor_id2
    : ∏ {a b : C} (f : a --> b), ##F (id2 f) = id2 (#F f)
    := pr1(pr2 F).

  Definition strict_psfunctor_vcomp
    : ∏ {a b : C} {f g h : C⟦a, b⟧} (η : f ==> g) (φ : g ==> h),
      ##F (η • φ) = ##F η • ##F φ
    := pr12(pr2 F).

  Definition strict_psfunctor_lunitor
    : ∏ {a b : C} (f : C⟦a, b⟧),
      lunitor (#F f)
      =
      (strict_psfunctor_id_cell F a ▹ #F f)
        • strict_psfunctor_comp_cell F (identity a) f
        • ##F (lunitor f)
    := pr122(pr2 F).

  Definition strict_psfunctor_runitor
    : ∏ {a b : C} (f : C⟦a, b⟧),
      runitor (#F f)
      =
      (#F f ◃ strict_psfunctor_id_cell F b)
        • strict_psfunctor_comp_cell F f (identity b)
        • ##F (runitor f)
    := pr1(pr222(pr2 F)).

  Definition strict_psfunctor_lassociator
    : ∏ {a b c d : C} (f : C⟦a, b⟧) (g : C⟦b, c⟧) (h : C⟦c, d⟧) ,
      (#F f ◃ strict_psfunctor_comp_cell F g h)
        • strict_psfunctor_comp_cell F f (g · h)
        • ##F (lassociator f g h)
      =
      (lassociator (#F f) (#F g) (#F h))
        • (strict_psfunctor_comp_cell F f g ▹ #F h)
        • strict_psfunctor_comp_cell F (f · g) h
    := pr12(pr222(pr2 F)).

  Definition strict_psfunctor_lwhisker
    : ∏ {a b c : C} (f : C⟦a, b⟧) {g₁ g₂ : C⟦b, c⟧} (η : g₁ ==> g₂),
      strict_psfunctor_comp_cell F f g₁ • ##F (f ◃ η)
      =
      #F f ◃ ##F η • strict_psfunctor_comp_cell F f g₂
    := pr122(pr222(pr2 F)).

  Definition strict_psfunctor_rwhisker
    : ∏ {a b c : C} {f₁ f₂ : C⟦a, b⟧} (g : C⟦b, c⟧) (η : f₁ ==> f₂),
      strict_psfunctor_comp_cell F f₁ g • ##F (η ▹ g)
      =
      ##F η ▹ #F g • strict_psfunctor_comp_cell F f₂ g
    := pr222(pr222(pr2 F)).
End StrictProjection.

Definition strict_psfunctor_is_iso
           {C D : bicat}
           (F : strict_psfunctor C D)
           {a b : C}
           {f g : C⟦a,b⟧}
           (α : invertible_2cell f g)
  : is_invertible_2cell (##F α).
Proof.
  use tpair.
  - exact (##F (α^-1)).
  - split ; cbn
    ; rewrite <- strict_psfunctor_vcomp, <- strict_psfunctor_id2 ; apply maponpaths.
    + apply vcomp_rinv.
    + apply vcomp_linv.
Defined.

Section StrictPseudoFunctorDerivedLaws.
  Context {C D : bicat}.
  Variable (F : strict_psfunctor C D).

  Definition strict_psfunctor_linvunitor
             {a b : C}
             (f : C⟦a, b⟧)
    : ##F (linvunitor f)
      =
      (linvunitor (#F f))
        • ((strict_psfunctor_id_cell F a) ▹ #F f)
        • (strict_psfunctor_comp_cell F _ _).
  Proof.
    rewrite !vassocl.
    cbn.
    use vcomp_move_L_pM.
    { is_iso. }
    cbn.
    use vcomp_move_R_Mp.
    {
      refine (strict_psfunctor_is_iso F (linvunitor f ,, _)).
      is_iso.
    }
    cbn.
    rewrite strict_psfunctor_lunitor ; cbn.
    rewrite <- !vassocr.
    reflexivity.
  Qed.

  Definition strict_psfunctor_rinvunitor
             {a b : C}
             (f : C⟦a, b⟧)
    : ##F (rinvunitor f)
      =
      (rinvunitor (#F f))
        • (#F f ◃ strict_psfunctor_id_cell F b)
        • strict_psfunctor_comp_cell F _ _.
  Proof.
    rewrite !vassocl.
    use vcomp_move_L_pM.
    { is_iso. }
    cbn.
    use vcomp_move_R_Mp.
    {
      refine (strict_psfunctor_is_iso F (rinvunitor f ,, _)).
      is_iso.
    }
    cbn.
    rewrite strict_psfunctor_runitor ; cbn.
    rewrite <- !vassocr.
    reflexivity.
  Qed.

  Definition strict_psfunctor_rassociator
             {a b c d : C}
             (f : C⟦a, b⟧) (g : C⟦b, c⟧) (h : C⟦c, d⟧)
    : (strict_psfunctor_comp_cell F f g ▹ #F h)
        • strict_psfunctor_comp_cell F (f · g) h
        • ##F (rassociator f g h)
      =
      (rassociator (#F f) (#F g) (#F h))
        • (#F f ◃ strict_psfunctor_comp_cell F g h)
        • strict_psfunctor_comp_cell F f (g · h).
  Proof.
    rewrite !vassocl.
    use vcomp_move_L_pM.
    { is_iso. }
    cbn.
    rewrite !vassocr.
    use vcomp_move_R_Mp.
    { refine (strict_psfunctor_is_iso F (rassociator f g h ,, _)).
      is_iso.
    }
    cbn.
    symmetry.
    exact (strict_psfunctor_lassociator F f g h).
  Qed.

  Definition strict_psfunctor_comp_natural
             {a b c : C}
             {g₁ g₂ : C⟦b,c⟧} {f₁ f₂ : C⟦a,b⟧}
             (ηg : g₁ ==> g₂) (ηf : f₁ ==> f₂)
    : strict_psfunctor_comp_cell F f₁ g₁ • ##F (ηf ⋆ ηg)
      =
      (##F ηf) ⋆ (##F ηg) • strict_psfunctor_comp_cell F f₂ g₂.
  Proof.
    unfold hcomp.
    rewrite !strict_psfunctor_vcomp.
    rewrite !vassocr.
    rewrite !strict_psfunctor_rwhisker.
    rewrite !vassocl.
    rewrite strict_psfunctor_lwhisker.
    reflexivity.
  Qed.

  Definition strict_psfunctor_F_lunitor
             {a b : C}
             (f : C⟦a, b⟧)
    : ##F (lunitor f)
      =
      ((strict_psfunctor_comp_cell F (identity a) f)^-1)
        • ((strict_psfunctor_id_cell F a)^-1 ▹ #F f)
        • lunitor (#F f).
  Proof.
    rewrite !vassocl.
    use vcomp_move_L_pM.
    { is_iso. }
    use vcomp_move_L_pM.
    { is_iso. }
    cbn.
    rewrite !vassocr.
    exact (!(strict_psfunctor_lunitor F f)).
  Qed.

  Definition strict_psfunctor_F_runitor
             {a b : C}
             (f : C⟦a,b⟧)
    : ##F (runitor f)
      =
      ((strict_psfunctor_comp_cell F f (identity b))^-1)
        • (#F f ◃ (strict_psfunctor_id_cell F b)^-1)
        • runitor (#F f).
  Proof.
    rewrite !vassocl.
    use vcomp_move_L_pM.
    { is_iso. }
    use vcomp_move_L_pM.
    { is_iso. }
    cbn.
    rewrite !vassocr.
    exact (!(strict_psfunctor_runitor F f)).
  Qed.
End StrictPseudoFunctorDerivedLaws.

Definition strict_pstrans_data
           {C D : bicat}
           (F G : strict_psfunctor C D)
  : UU.
Proof.
  refine (map1cells C D⟦_,_⟧).
  - apply F.
  - apply G.
Defined.

Definition is_strict_pstrans
           {C D : bicat}
           {F G : strict_psfunctor C D}
           (η : strict_pstrans_data F G)
  : UU
  := (∏ (X Y : C) (f g : X --> Y) (α : f ==> g),
      (pr1 η X ◃ ##G α)
        • pr2 η _ _ g
      =
      (pr2 η _ _ f)
        • (##F α ▹ pr1 η Y))
       ×
       (∏ (X : C),
        (pr1 η X ◃ strict_psfunctor_id_cell G X)
          • pr2 η _ _ (id₁ X)
        =
        (runitor (pr1 η X))
          • linvunitor (pr1 η X)
          • (strict_psfunctor_id_cell F X ▹ pr1 η X))
       ×
       (∏ (X Y Z : C) (f : X --> Y) (g : Y --> Z),
        (pr1 η X ◃ strict_psfunctor_comp_cell G f g)
          • pr2 η _ _ (f · g)
        =
        (lassociator (pr1 η X) (#G f) (#G g))
          • (pr2 η _ _ f ▹ (#G g))
          • rassociator (#F f) (pr1 η Y) (#G g)
          • (#F f ◃ pr2 η _ _ g)
          • lassociator (#F f) (#F g) (pr1 η Z)
          • (strict_psfunctor_comp_cell F f g ▹ pr1 η Z)).

Definition make_strict_pstrans
           {C D : bicat}
           {F G : strict_psfunctor C D}
           (η : strict_pstrans_data F G)
           (Hη : is_strict_pstrans η)
  : F --> G.
Proof.
  refine ((η ,, _) ,, tt).
  repeat split ; cbn ; intros ; apply Hη.
Defined.

Definition strict_modification_eq
           {B B' : bicat}
           {F G : strict_psfunctor B B'}
           {σ τ : F --> G}
           {m m' : σ ==> τ}
           (p : ∏ (X : B), pr111 m X = pr111 m' X)
  : m = m'.
Proof.
  use subtypePath.
  { intro. simpl.
    exact isapropunit.
  }
  use subtypePath.
  { intro. simpl.
    repeat (apply isapropdirprod) ; apply isapropunit.
  }
  use subtypePath.
  { intro. simpl.
    repeat (apply impred ; intro).
    apply B'.
  }
  use funextsec.
  exact p.
Qed.

Definition is_strict_modification
           {B B' : bicat}
           {F G : strict_psfunctor B B'}
           {σ τ : F --> G}
           (m : ∏ (X : B), pr111 σ X ==> pr111 τ X)
  : UU
  := ∏ (X Y : B) (f : X --> Y),
     pr211 σ _ _ f • (m Y ▻ #F f)
     =
     #G f ◅ m X • pr211 τ _ _ f.

Definition make_strict_modification
           {B B' : bicat}
           {F G : strict_psfunctor B B'}
           {σ τ : F --> G}
           (m : ∏ (X : B), pr111 σ X ==> pr111 τ X)
           (Hm : is_strict_modification m)
  : σ ==> τ
  := (((m ,, Hm) ,, (tt ,, tt ,, tt)),, tt).

Definition make_is_invertible_strict_modification_inv_is_modification
           {B B' : bicat}
           {F G : strict_psfunctor B B'}
           {σ τ : F --> G}
           (m : σ ==> τ)
           (Hm : ∏ (X : B), is_invertible_2cell (pr111 m X))
  : ∏ (X Y : B) (f : B ⟦ X, Y ⟧),
    (pr211 τ) X Y f • (# F f ◃ (Hm Y) ^-1) = ((Hm X) ^-1 ▹ # G f) • (pr211 σ) X Y f.
Proof.
  intros X Y f.
  simpl.
  use vcomp_move_R_Mp.
  { is_iso. }
  simpl.
  rewrite <- vassocr.
  use vcomp_move_L_pM.
  { is_iso. }
  symmetry.
  simpl.
  exact (pr211 m X Y f).
Qed.

Definition inv_modification
           {B B' : bicat}
           {F G : strict_psfunctor B B'}
           {σ τ : F --> G}
           (m : σ ==> τ)
           (Hm : ∏ (X : B), is_invertible_2cell (pr111 m X))
  : τ ==> σ.
Proof.
  use make_strict_modification.
  - exact (λ X, (Hm X)^-1).
  - exact (make_is_invertible_strict_modification_inv_is_modification m Hm).
Defined.

Definition modification_inv_modification
           {B B' : bicat}
           {F G : strict_psfunctor B B'}
           {σ τ : F --> G}
           (m : σ ==> τ)
           (Hm : ∏ (X : B), is_invertible_2cell (pr111 m X))
  : m • inv_modification m Hm = id₂ σ.
Proof.
  use strict_modification_eq.
  intro X.
  cbn.
  exact (vcomp_rinv (Hm X)).
Qed.

Definition inv_modification_modification
           {B B' : bicat}
           {F G : strict_psfunctor B B'}
           {σ τ : F --> G}
           (m : σ ==> τ)
           (Hm : ∏ (X : B), is_invertible_2cell (pr111 m X))
  : inv_modification m Hm • m = id₂ τ.
Proof.
  use strict_modification_eq.
  intro X.
  cbn.
  exact (vcomp_linv (Hm X)).
Qed.

Definition make_is_invertible_strict_modification
           {B B' : bicat}
           {F G : strict_psfunctor B B'}
           {σ τ : F --> G}
           (m : σ ==> τ)
           (Hm : ∏ (X : B), is_invertible_2cell (pr111 m X))
  : is_invertible_2cell m.
Proof.
  use make_is_invertible_2cell.
  - exact (inv_modification m Hm).
  - exact (modification_inv_modification m Hm).
  - exact (inv_modification_modification m Hm).
Defined.

Module Notations.
  Notation "'##'" := (strict_psfunctor_on_cells).
End Notations.