Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.functor_categories.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.HorizontalComposition.

Require Import UniMath.CategoryTheory.Bicategories.WkCatEnrichment.prebicategory.
Require Import UniMath.CategoryTheory.Bicategories.WkCatEnrichment.whiskering.

Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Bicat. Import Bicat.Notations.
Require Import UniMath.CategoryTheory.Bicategories.WkCatEnrichment.Notations.

Local Open Scope cat.


Lemma whisker_left_left {C : prebicategory} {a b c d : C}
      (f : a -1-> b) (g : b -1-> c) {h i : c -1-> d} (x : h -2-> i) :
  whisker_left f (whisker_left g x) ;v; associator_2mor f g i =
  associator_2mor f g h ;v; whisker_left (f ;1; g) x.
Proof.
  unfold whisker_left.
  etrans; [ apply associator_naturality | idtac].
  apply maponpaths.
  apply maponpaths_2.
  exact horizontal_comp_id.
Defined.

Lemma whisker_left_right {C : prebicategory} {a b c d : C}
      (f : a -1-> b) (g h : b -1-> c) (i : c -1-> d) (x : g -2-> h) :
  whisker_left f (whisker_right x i) ;v; associator_2mor f h i =
  associator_2mor f g i ;v; whisker_right (whisker_left f x) i.
Proof.
  exact (associator_naturality (identity f) x (identity i)).
Defined.

Lemma whisker_right_right {C : prebicategory} {a b c d : C}
      (f g : a -1-> b) (h : b -1-> c) (i : c -1-> d) (x : f -2-> g) :
  associator_2mor f h i ;v; whisker_right (whisker_right x h) i =
  whisker_right x (h ;1; i) ;v; associator_2mor g h i.
Proof.
  unfold whisker_right.
  etrans; [ apply pathsinv0, associator_naturality | idtac].
  apply maponpaths_2, maponpaths.
  exact horizontal_comp_id.
Defined.


Section unfold_data.

Variable C : prebicategory.

Definition bcat_precategory_ob_mor : precategory_ob_mor.
Proof.
  ∃ C. exact (λ a b, homprecat a b).
Defined.

Definition bcat_cell_struct : prebicat_2cell_struct bcat_precategory_ob_mor
  := λ (a b : C) (f g : homprecat a b), (homprecat a b) ⟦ f, g ⟧.

Definition bcat_ob_mor_cells : ∑ (C : precategory_ob_mor), prebicat_2cell_struct C.
Proof.
  ∃ bcat_precategory_ob_mor. exact bcat_cell_struct.
Defined.

Definition bcat_1_id_comp_cells : prebicat_1_id_comp_cells.
Proof.
  use tpair.
  - ∃ bcat_precategory_ob_mor.
    use tpair.
    + simpl. intros. exact (identity1 _).
    + simpl. intros a b c f g. exact (compose1 f g).
  - exact bcat_cell_struct.
Defined.


Definition bcat_2_id_comp_struct : prebicat_2_id_comp_struct bcat_1_id_comp_cells.
Proof.
  repeat split; simpl; unfold bcat_cell_struct.
  -
    intros. exact (identity _).
  -
    intros. exact (left_unitor f).
  -
    intros. exact (right_unitor f).
  -
    intros. exact (inv_from_iso (left_unitor f)).
  -
    intros. exact (inv_from_iso (right_unitor f)).
  -
    intros. exact (inv_from_iso (associator f g h)).
  -
    intros. exact (associator_2mor f g h).
  -
    intros a b f g h x y. exact (x · y).
  -
    intros a b c f g1 g2 x. exact (whisker_left f x).
  -
    intros a b c f1 f2 g x. exact (whisker_right x g).
Defined.

Definition bcat_data : ∑ C, prebicat_2_id_comp_struct C.
Proof.
  ∃ bcat_1_id_comp_cells. exact bcat_2_id_comp_struct.
Defined.

Theorem bcat_laws : prebicat_laws bcat_data.
Proof.
  repeat split;
  unfold id2, vcomp2, runitor, lunitor, rinvunitor, linvunitor,
         rassociator, lassociator, lwhisker, rwhisker;
  simpl;
  unfold bcat_precategory_ob_mor, bcat_cell_struct, bcat_ob_mor_cells,
         bcat_1_id_comp_cells, bcat_2_id_comp_struct, bcat_data;
  simpl;
  first [ intros until 1 | intros ].
  -
    apply id_left.
  -
    apply id_right.
  -
    apply assoc.
  -
    apply whisker_left_id_2mor.
  -
    apply whisker_right_id_2mor.
  -
    apply pathsinv0, whisker_left_on_comp.
  -
    apply pathsinv0, whisker_right_on_comp.
  -
    apply left_unitor_naturality.
  -
    apply right_unitor_naturality.
  -
    apply whisker_left_left.
  -
    apply whisker_left_right.
  -
    apply whisker_right_right.
  -
    apply twomor_naturality.
  -
    apply (iso_inv_after_iso (left_unitor f)).
  -
    apply (iso_after_iso_inv (left_unitor f)).
  -
    apply (iso_inv_after_iso (right_unitor f)).
  -
    apply (iso_after_iso_inv (right_unitor f)).
  -
    apply (iso_inv_after_iso (associator f g h)).
  -
    apply (iso_after_iso_inv (associator f g h)).
  -
    apply pathsinv0, (triangle_axiom f g).
  -
    apply pathsinv0, (pentagon_axiom f g h).
Defined.

Definition bcat : prebicat := (bcat_data,, bcat_laws).

End unfold_data.