Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.

Local Open Scope cat.

Definition two_cat_data
  : UU
  := ∑ (C : category)
       (cells_C : ∏ (x y : C), x --> y → x --> y → UU),
     (∏ (x y : C) (f : x --> y), cells_C _ _ f f)
     × (∏ (x y : C) (f g h : x --> y),
        cells_C _ _ f g → cells_C _ _ g h → cells_C _ _ f h)
     × (∏ (x y z : C)
          (f : x --> y)
          (g1 g2 : y --> z),
        cells_C _ _ g1 g2 → cells_C _ _ (f · g1) (f · g2))
     × (∏ (x y z : C)
          (f1 f2 : x --> y)
          (g : y --> z),
        cells_C _ _ f1 f2 → cells_C _ _ (f1 · g) (f2 · g)).

Coercion category_from_two_cat_data (C : two_cat_data)
  : category
  := pr1 C.

Definition two_cat_cells
           (C : two_cat_data)
           {a b : C}
           (f g : C⟦a, b⟧)
  : UU
  := pr12 C a b f g.

Local Notation "f '==>' g" := (two_cat_cells _ f g) (at level 60).
Local Notation "f '<==' g" := (two_cat_cells _ g f) (at level 60, only parsing).

Definition id2 {C : two_cat_data} {a b : C} (f : C⟦a, b⟧) : f ==> f
  := pr122 C a b f.

Definition vcomp2 {C : two_cat_data} {a b : C} {f g h : C⟦a, b⟧}
  : f ==> g → g ==> h → f ==> h
  := λ x y, pr1 (pr222 C) _ _ _ _ _ x y.

Definition lwhisker {C : two_cat_data} {a b c : C} (f : C⟦a, b⟧) {g1 g2 : C⟦b, c⟧}
  : g1 ==> g2 → f · g1 ==> f · g2
  := λ x, pr12 (pr222 C) _ _ _ _ _ _ x.

Definition rwhisker {C : two_cat_data} {a b c : C} {f1 f2 : C⟦a, b⟧} (g : C⟦b, c⟧)
  : f1 ==> f2 → f1 · g ==> f2 · g
  := λ x, pr22 (pr222 C) _ _ _ _ _ _ x.

Local Notation "x • y" := (vcomp2 x y) (at level 60).
Local Notation "f ◃ x" := (lwhisker f x) (at level 60). Local Notation "y ▹ g" := (rwhisker g y) (at level 60).
Definition hcomp {C : two_cat_data} {a b c : C} {f1 f2 : C⟦a, b⟧} {g1 g2 : C⟦b, c⟧}
  : f1 ==> f2 → g1 ==> g2 → f1 · g1 ==> f2 · g2
  := λ x y, (x ▹ g1) • (f2 ◃ y).

Definition hcomp' {C : two_cat_data} {a b c : C} {f1 f2 : C⟦a, b⟧} {g1 g2 : C⟦b, c⟧}
  : f1 ==> f2 → g1 ==> g2 → f1 · g1 ==> f2 · g2
  := λ x y, (f1 ◃ y) • (x ▹ g2).

Local Notation "x ⋆ y" := (hcomp x y) (at level 50, left associativity).

Definition two_cat_laws (C : two_cat_data)
  : UU
  :=

       (∏ (a b : C) (f g : C⟦a, b⟧) (x : f ==> g), id2 f • x = x)
     ×

       (∏ (a b : C) (f g : C⟦a, b⟧) (x : f ==> g), x • id2 g = x)
     ×

       (∏ (a b : C) (f g h k : C⟦a, b⟧) (x : f ==> g) (y : g ==> h) (z : h ==> k),
        x • (y • z) = (x • y) • z)
     ×

       (∏ (a b c : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧), f ◃ id2 g = id2 _)
     ×

       (∏ (a b c : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧), id2 f ▹ g = id2 _)
     ×

       (∏ (a b c : C) (f : C⟦a, b⟧) (g h i : C⟦b, c⟧) (x : g ==> h) (y : h ==> i),
        (f ◃ x) • (f ◃ y) = f ◃ (x • y))
     ×

       (∏ (a b c : C) (f g h : C⟦a, b⟧) (i : C⟦b, c⟧) (x : f ==> g) (y : g ==> h),
        (x ▹ i) • (y ▹ i) = (x • y) ▹ i)
     ×

       (∏ (a b c : C) (f g : C⟦a, b⟧) (h i : C⟦b, c⟧) (x : f ==> g) (y : h ==> i),
        (x ▹ h) • (g ◃ y) = (f ◃ y) • (x ▹ i)).

Definition two_precat : UU := ∑ C : two_cat_data, two_cat_laws C.

Coercion two_cat_data_from_two_cat (C : two_precat) : two_cat_data := pr1 C.
Coercion two_cat_laws_from_two_cat (C : two_precat) : two_cat_laws C := pr2 C.

Section two_cat_law_projections.

Context {C : two_precat}.

Definition id2_left {a b : C} {f g : C⟦a, b⟧} (x : f ==> g)
  : id2 f • x = x
  := pr1 (pr2 C) _ _ _ _ x.

Definition id2_right {a b : C} {f g : C⟦a, b⟧} (x : f ==> g)
  : x • id2 g = x
  := pr1 (pr2 (pr2 C)) _ _ _ _ x.

Definition vassocr {a b : C} {f g h k : C⟦a, b⟧}
           (x : f ==> g) (y : g ==> h) (z : h ==> k)
  : x • (y • z) = (x • y) • z
  := pr1 (pr2 (pr2 (pr2 C))) _ _ _ _ _ _ x y z.

Definition lwhisker_id2 {a b c : C} (f : C⟦a, b⟧) (g : C⟦b, c⟧)
  : f ◃ id2 g = id2 _
  := pr1 (pr2 (pr2 (pr2 (pr2 C)))) _ _ _ f g.

Definition id2_rwhisker {a b c : C} (f : C⟦a, b⟧) (g : C⟦b, c⟧)
  : id2 f ▹ g = id2 _
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 C))))) _ _ _ f g.

Definition lwhisker_vcomp {a b c : C} (f : C⟦a, b⟧) {g h i : C⟦b, c⟧}
           (x : g ==> h) (y : h ==> i)
  : (f ◃ x) • (f ◃ y) = f ◃ (x • y)
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))) _ _ _ f _ _ _ x y.

Definition rwhisker_vcomp {a b c : C} {f g h : C⟦a, b⟧}
           (i : C⟦b, c⟧) (x : f ==> g) (y : g ==> h)
  : (x ▹ i) • (y ▹ i) = (x • y) ▹ i
  := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C))))))) _ _ _ _ _ _ i x y.

Definition vcomp_whisker {a b c : C} {f g : C⟦a, b⟧} {h i : C⟦b, c⟧}
           (x : f ==> g) (y : h ==> i)
  : (x ▹ h) • (g ◃ y) = (f ◃ y) • (x ▹ i)
  := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C))))))) _ _ _ _ _ _ i x y.
End two_cat_law_projections.

Definition isaset_cells (C : two_precat) : UU
  := ∏ (a b : C) (f g : a --> b), isaset (f ==> g).

Definition two_cat : UU
  := ∑ C : two_precat, isaset_cells C.