Library UniMath.Bicategories.Core.Examples.BicategoryFromWhiskeredMonoidal

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.MonoidalCategoriesWhiskered.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.Bicategories.Core.Bicat.

Local Open Scope cat.

Section Bicat_From_Monoidal_Cat.

Import Bicat.Notations.
Import BifunctorNotations.

Context {C: category} (M : monoidal C).

Definition one_cells_data_from_monoidal : precategory_data.
Proof.
  use tpair.
  - exact (unit ,, (λ _ _, ob C)).
  - split.
    + intros dummy. exact I_{ M }.
    + intros dummy0 dummy1 dummy2. exact (λ a b, a ⊗_{M} b).
Defined.

Definition two_cells_from_monoidal : prebicat_2cell_struct (one_cells_data_from_monoidal)
  := λ _ _ a b, C ⟦ a , b⟧.

Definition prebicat_data_from_monoidal : prebicat_data.
Proof.
  use make_prebicat_data.
  - exact (one_cells_data_from_monoidal ,, two_cells_from_monoidal).
  - split. { intros ? ? f. exact (id₁ f). }
    split. { intros ? ? f. apply monoidal_leftunitordata. }
    split. { intros ? ? f. apply monoidal_rightunitordata. }
    split. { intros ? ? f. apply (is_z_isomorphism_mor (leftunitorlaw_iso (monoidal_leftunitorlaw M) f)). }
    split. { intros ? ? f. apply (is_z_isomorphism_mor (rightunitorlaw_iso (monoidal_rightunitorlaw M) f)). }
    split. { intros ? ? ? ? f g h. exact ( α_{ M } f g h ). }
    split. { intros ? ? ? ? f g h. apply (is_z_isomorphism_mor (associatorlaw_iso (monoidal_associatorlaw M) f g h)). }
    split. { intros ? ? f g h. exact compose. }
    split. { intros ? ? ? f g h. exact (λ u, (f ⊗^{ M }_{l} u)). }
             intros ? ? ? f g h. exact (λ u, (u ⊗^{ M }_{r} h)).
Defined.

Lemma prebicat_laws_from_monoidal : prebicat_laws (prebicat_data_from_monoidal).
Proof.
  split. { intros. apply id_left. }
  split. { intros. apply id_right. }

  
  split. { intros. apply assoc. }

  
  split. { intros ? ? ? f g. apply bifunctor_leftid. }
  split. { intros ? ? ? f g. apply bifunctor_rightid. }

  
  split. {
    intros ? ? ? f g h i x y.
    apply pathsinv0, bifunctor_leftcomp.
  }

  
  split. {
    intros ? ? ? f g h i x y.
    apply pathsinv0, bifunctor_rightcomp.
  }

  
  split. { intros. apply (leftunitorlaw_nat (monoidal_leftunitorlaw M)). }
  split. { intros. apply (rightunitorlaw_nat (monoidal_rightunitorlaw M)). }

  
  split. {
    intros ? ? ? ? f g h i x.
    cbn.
    apply pathsinv0.
    apply (z_iso_inv_on_right _ _ _ (_,,associatorlaw_iso (monoidal_associatorlaw M) f g h)).
    rewrite assoc.
    apply (z_iso_inv_on_left _ _ _ _ (_,,associatorlaw_iso (monoidal_associatorlaw M) f g i)).
    apply (associatorlaw_natleft (monoidal_associatorlaw M)).
  }

  
  split. {
    intros ? ? ? ? f g h i x.
    cbn.
    apply pathsinv0.
    apply (z_iso_inv_on_right _ _ _ (_,,associatorlaw_iso (monoidal_associatorlaw M) f g i)).
    rewrite assoc.
    apply (z_iso_inv_on_left _ _ _ _ (_,,associatorlaw_iso (monoidal_associatorlaw M) f h i)).
    apply (associatorlaw_natleftright (monoidal_associatorlaw M)).
  }

  
  split. {
    intros ? ? ? ? f g h i x.
    cbn.
    apply (z_iso_inv_on_right _ _ _ (_,,associatorlaw_iso (monoidal_associatorlaw M) f h i)).
    rewrite assoc.
    apply (z_iso_inv_on_left _ _ _ _ (_,,associatorlaw_iso (monoidal_associatorlaw M) g h i)).
    apply (associatorlaw_natright (monoidal_associatorlaw M)).
  }

  
  split. {
    intros.
    cbn.
    apply bifunctor_equalwhiskers.
  }

  
  split. { intros ? ? f. exact (pr12 (leftunitorlaw_iso (monoidal_leftunitorlaw M) f)). }
  split. { intros ? ? f. exact (pr22 (leftunitorlaw_iso (monoidal_leftunitorlaw M) f)). }

  
  split. { intros ? ? f. exact (pr12 (rightunitorlaw_iso (monoidal_rightunitorlaw M) f)). }
  split. { intros ? ? f. exact (pr22 (rightunitorlaw_iso (monoidal_rightunitorlaw M) f)). }

  
  split. { intros ? ? ? ? f g h. exact (pr22 (associatorlaw_iso (monoidal_associatorlaw M) f g h)). }
  split. { intros ? ? ? ? f g h. exact (pr12 (associatorlaw_iso (monoidal_associatorlaw M) f g h)). }

  
  split. {
    intros ? ? ? f g.
    apply (z_iso_inv_on_right _ _ _ (_,,associatorlaw_iso (monoidal_associatorlaw M) f I_{ M} g)).
    apply pathsinv0, monoidal_triangleidentity.
  }

  
  intros ? ? ? ? ? f g h i.
  cbn.
  apply pentagon_identity_leftassociator.
Qed.

Definition prebicat_from_monoidal : prebicat :=
  prebicat_data_from_monoidal ,, prebicat_laws_from_monoidal.

Definition bicat_from_monoidal : bicat.
  use build_bicategory.
  - exact prebicat_data_from_monoidal.
  - exact prebicat_laws_from_monoidal.
  - red. intros. apply homset_property.
Defined.

End Bicat_From_Monoidal_Cat.