Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.TotalDisplayedMonoidalCurried


Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesCurried.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.DisplayedMonoidalCurried.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsCurried.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.

Local Open Scope cat.
Local Open Scope mor_disp_scope.

Section MonoidalTotalCategory.

  Context (C : category) (T : tensor_data C) (I : C) (α : associator_data T) (lu : leftunitor_data T I) (ru : rightunitor_data T I) (tid : tensorfunctor_id T) (tcomp : tensorfunctor_comp T) (αnat : associator_naturality α) (αiso : associator_is_natiso α) (lunat : leftunitor_naturality lu) (luiso : leftunitor_is_natiso lu) (runat : rightunitor_naturality ru) (ruiso : rightunitor_is_natiso ru) (tri : triangle_identity lu ru α) (pen : pentagon_identity α)
          (D : disp_cat C) (dtd : displayedtensor_data C D T) (i : D I) (dα : displayedassociator_data C D T α dtd) (dlu : displayedleftunitor_data C D T I lu dtd i) (dru : displayedrightunitor_data C D T I ru dtd i) (dtid : displayedtensor_id C D T tid dtd) (dtcomp : displayedtensor_comp C D T tcomp dtd) (dαnat : displayedassociator_naturality C D T α αnat dα ) (dαiso : displayedassociator_is_nat_iso C D T α αiso dα ) (dlunat : displayedleftunitor_naturality C D T I lu lunat dlu ) (dluiso : displayedleftunitor_is_nat_iso C D T I lu luiso dlu) (drunat : displayedrightunitor_naturality C D T I ru runat dru ) (druiso : displayedrightunitor_is_nat_iso C D T I ru ruiso dru) (dtri : displayedtriangle_identity C D T I α lu ru tri dlu dru dα) (dpen : displayedpentagon_identity C D T α pen dα).

  Notation ToD := (total_category D).
  Notation "x ⊗_{ T } y" := (tensoronobjects_from_tensordata T x y) (at level 31).
  Notation "f ⊗^{ T } g" := (tensoronmorphisms_from_tensordata T _ _ _ _ f g) (at level 31).
  Notation "a ⊗_{{ dtd }} b" := (displayedtensoronobjects_from_displayedtensordata _ _ _ dtd _ _ a b) (at level 31).
  Notation "f' ⊗^{{ dtd }} g'" := (displayedtensoronmorphisms_from_displayedtensordata dtd _ _ _ _ _ _ _ _ _ _ f' g' ) (at level 31).

DATA
  Definition totalcategory_tensordata : tensor_data ToD.
  Show proof.
    use tpair.
    + intros xa yb.
      exact ((pr1 xa) ⊗_{T} (pr1 yb) ,, (pr2 xa) ⊗_{{dtd}} (pr2 yb)).
    + intros xa yb xa' yb' f g.
       split with (pr1 f ⊗^{T} pr1 g).
       apply (pr2 dtd).
       - exact (pr2 f).
       - exact (pr2 g).
  Notation TtD := totalcategory_tensordata.

  Definition totalcategory_associatordata : associator_data TtD.
  Show proof.
    intros x y z.
    use tpair.
    + exact (α (pr1 x) (pr1 y) (pr1 z)).
    + exact (dα (pr1 x) (pr1 y) (pr1 z) (pr2 x) (pr2 y) (pr2 z)).
  Notation TαD := totalcategory_associatordata.

  Definition totalcategory_unitdata : ToD := (I,,i).
  Notation TuD := totalcategory_unitdata.

  Definition totalcategory_leftunitordata : leftunitor_data TtD TuD.
  Show proof.
    intro x.
    use tpair.
    + apply lu.
    + exact (dlu (pr1 x) (pr2 x)).
  Notation TluD := totalcategory_leftunitordata.

  Definition totalcategory_rightunitordata : rightunitor_data TtD TuD.
  Show proof.
    intro x.
    use tpair.
    + apply ru.
    + exact (dru (pr1 x) (pr2 x)).
  Notation TruD := totalcategory_rightunitordata.

  Definition totalcategory_monoidalcatdata : (monoidalcategory_data ToD) := (TtD,,TuD,,TluD,,TruD,,TαD).

PROPERTIES
  Lemma totalcategory_tensorfunctorid : tensorfunctor_id TtD.
  Show proof.
    intros x y.
    use total2_paths_b.
    + apply tid.
    + apply (dtid (pr1 x) (pr1 y) (pr2 x) (pr2 y)).

  Lemma totalcategory_tensorfunctorcomp : tensorfunctor_comp TtD.
  Show proof.
    intros x y x' y' x'' y'' f f' g g'.
    use total2_paths_b.
    + use tcomp.
    + use (((dtcomp (pr1 x) (pr1 y) (pr1 x') (pr1 y') (pr1 x'') (pr1 y'')
                         (pr2 x) (pr2 y) (pr2 x') (pr2 y') (pr2 x'') (pr2 y'')
                         (pr1 f) (pr1 g) (pr1 f') (pr1 g')
                         (pr2 f) (pr2 g) (pr2 f') (pr2 g')))).

  Lemma totalcategory_associatornaturality : associator_naturality TαD.
  Show proof.
    intros x x' y y' z z' f g h.
    use total2_paths_b.
    - exact (αnat (pr1 x) (pr1 x') (pr1 y) (pr1 y') (pr1 z) (pr1 z') (pr1 f) (pr1 g) (pr1 h)).
    - exact (dαnat (pr1 x) (pr1 x') (pr1 y) (pr1 y') (pr1 z) (pr1 z')
                        (pr2 x) (pr2 x') (pr2 y) (pr2 y') (pr2 z) (pr2 z')
                        (pr1 f) (pr1 g) (pr1 h) (pr2 f) (pr2 g) (pr2 h)).

End MonoidalTotalCategory.