Library UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory

Going into the opposite direction of UniMath.Bicategories.Core.Examples.BicategoryFromMonoidal

We fix a bicategory and an object of it and construct the monoidal category of endomorphisms.
Written by Ralph Matthes in 2019.

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.AlternativeDefinitions.MonoidalCategoriesTensored.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.Bicategories.Core.Bicat.

Local Open Scope cat.

Section Monoidal_Cat_From_Bicat.

Local Open Scope bicategory_scope.
Import Bicat.Notations.

Context {C : bicat}.
Context (c0: ob C).

Definition precategory_data_from_bicat_and_ob: precategory_data.
Show proof.
  use make_precategory_data.
  - use make_precategory_ob_mor.
    + exact (C⟦c0,c0⟧).
    + apply prebicat_cells.
  - intro c; apply id2.
  - intros a b c; apply vcomp2.

Lemma is_precategory_data_from_prebicat_and_ob: is_precategory precategory_data_from_bicat_and_ob.
Show proof.
  use make_is_precategory.
  - intros a b f; apply id2_left.
  - intros a b f; apply id2_right.
  - intros a b c d f g h; apply vassocr.
  - intros a b c d f g h; apply pathsinv0; apply vassocr.

Definition precategory_from_bicat_and_ob: precategory := _,, is_precategory_data_from_prebicat_and_ob.

Lemma has_homsets_precategory_from_bicat_and_ob: has_homsets precategory_from_bicat_and_ob.
Show proof.
  red. intros.
  apply (cellset_property(C:=C)).

Definition category_from_bicat_and_ob: category := precategory_from_bicat_and_ob ,, has_homsets_precategory_from_bicat_and_ob.

Local Notation EndC := category_from_bicat_and_ob.

Definition tensor_from_bicat_and_ob: category_from_bicat_and_ob ⊠ category_from_bicat_and_ob ⟶ category_from_bicat_and_ob.
Show proof.
  use make_functor.
  - use make_functor_data.
    + intro ab.
      exact (pr1 ab · pr2 ab).
    + intros ab1 ab2 f.
      exact (hcomp (pr1 f) (pr2 f)).
  - abstract ( split; [ intro c; apply hcomp_identity |
                        intros a b c f g; apply hcomp_vcomp ] ).

Local Notation tensor := tensor_from_bicat_and_ob.

Local Definition build_left_unitor: left_unitor tensor (id c0).
Show proof.
  use make_nat_z_iso.
  + use make_nat_trans.
    * intro c.
      apply lunitor.
    * abstract ( intros a b f; apply lunitor_natural ).
  + intro c; apply is_z_iso_lunitor.

Local Definition build_right_unitor: right_unitor tensor (id c0).
Show proof.
  use make_nat_z_iso.
  + use make_nat_trans.
    * intro c.
      apply runitor.
    * abstract ( intros a b f; apply runitor_natural ).
  + intro c; apply is_z_iso_runitor.

Definition nat_trans_associator: assoc_left tensor ⟹ assoc_right tensor.
Show proof.
  exists rassociator_fun'.
  abstract (intros f g x; apply hcomp_rassoc).

Local Definition build_associator: associator tensor.
Show proof.
  use make_nat_z_iso.
  - exact nat_trans_associator.
  - intro c; apply is_z_iso_rassociator.

Definition monoidal_cat_from_bicat_and_ob: monoidal_cat.
Show proof.
  use (make_monoidal_cat category_from_bicat_and_ob tensor_from_bicat_and_ob (id c0) build_left_unitor build_right_unitor build_associator).
  - abstract ( intros a b; apply pathsinv0; apply unit_triangle ).
  - abstract ( intros a b c d; apply pathsinv0; apply associativity_pentagon ).

End Monoidal_Cat_From_Bicat.