Library UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.AssociatorUnitorsLayer


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

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.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.

Require Import UniMath.Bicategories.Core.Bicat.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat.
Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sigma.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat.
Require Import UniMath.Bicategories.Core.Univalence.

Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories.
Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.TensorLayer.
Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.UnitLayer.
Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.TensorUnitLayer.

Local Open Scope cat.
Local Open Scope mor_disp_scope.

Section LeftUnitorLayer.

  Definition disp_lu_disp_ob_mor : disp_cat_ob_mor tu_cat.
  Show proof.
    use tpair.
    - exact (λ C, lunitor (tu C)).
    - exact (λ C D luC luD F, preserves_lunitor (ftu F) luC luD).

  Definition disp_lu_disp_id_comp : disp_cat_id_comp tu_cat disp_lu_disp_ob_mor.
  Show proof.
    use tpair.
    - intros C lu.
      apply id_preserves_lunitor.
    - intros C D E F G luC luD luE pluF pluG x.
      apply (comp_preserves_lunitor pluF pluG).

  Definition disp_lu_disp_cat_data : disp_cat_data tu_cat
    := (disp_lu_disp_ob_mor,, disp_lu_disp_id_comp).

  Definition bidisp_lu_disp_bicat : disp_bicat tu_cat
    := disp_cell_unit_bicat disp_lu_disp_cat_data.

  Lemma bidisp_lu_disp_prebicat_is_locally_univalent : disp_univalent_2_1 bidisp_lu_disp_bicat.
  Show proof.
    apply disp_cell_unit_bicat_univalent_2_1.
    intro ; intros.
    apply isaprop_preserves_lunitor.

  Lemma isaset_lunitor (C : tu_cat) : isaset (lunitor (pr2 C)).
  Show proof.
    apply isaset_total2.
    {
      apply impred_isaset ; intro.
      apply homset_property.
    }
    intro.
    repeat (apply impred_isaset ; intro).
    apply isasetaprop.
    apply homset_property.

  Lemma isaprop_lunitor_nat (C : tu_cat) (lu : lunitor (pr2 C)) : isaprop (lunitor_nat (pr1 lu)).
  Show proof.
    repeat (apply impred_isaprop ; intro).
    apply homset_property.

  Lemma bidisp_lu_disp_prebicat_is_globally_univalent : disp_univalent_2_0 bidisp_lu_disp_bicat.
  Show proof.
    apply disp_cell_unit_bicat_univalent_2_0.
    - apply bidisp_tensorunit_is_univalent_2.
    - intro ; intros.
      apply isaprop_preserves_lunitor.
    - intro ; apply isaset_lunitor.
    - intros C lu1 lu2 plu.
      use total2_paths_f.
      + apply funextsec ; intro.
        refine (_ @ (pr1 plu x)).
        refine (! id_left _ @ _).
        apply cancel_postcomposition.
        refine (_ @ ! id_right _).
        apply (! tensor_id _ _ _).
      + apply isaprop_lunitor_nat.

  Lemma bidisp_lu_disp_prebicat_is_univalent_2 : disp_univalent_2 bidisp_lu_disp_bicat.
  Show proof.

End LeftUnitorLayer.

Section RightUnitorLayer.

  Definition disp_ru_disp_ob_mor : disp_cat_ob_mor tu_cat.
  Show proof.
    use tpair.
    - exact (λ C, runitor (tu C)).
    - exact (λ C D ruC ruD F, preserves_runitor (ftu F) ruC ruD).

  Definition disp_ru_disp_id_comp : disp_cat_id_comp tu_cat disp_ru_disp_ob_mor.
  Show proof.
    use tpair.
    - intros C ru.
      apply id_preserves_runitor.
    - intros C D E F G ruC ruD ruE pruF pruG x.
      apply (comp_preserves_runitor pruF pruG).

  Definition disp_ru_disp_cat_data : disp_cat_data tu_cat
    := (disp_ru_disp_ob_mor,, disp_ru_disp_id_comp).

  Definition bidisp_ru_disp_bicat : disp_bicat tu_cat
    := disp_cell_unit_bicat disp_ru_disp_cat_data.

  Lemma bidisp_ru_disp_prebicat_is_locally_univalent : disp_univalent_2_1 bidisp_ru_disp_bicat.
  Show proof.
    apply disp_cell_unit_bicat_univalent_2_1.
    intro ; intros.
    apply isaprop_preserves_runitor.

  Lemma isaset_runitor (C : tu_cat) : isaset (runitor (pr2 C)).
  Show proof.
    apply isaset_total2.
    {
      apply impred_isaset ; intro.
      apply homset_property.
    }
    intro.
    repeat (apply impred_isaset ; intro).
    apply isasetaprop.
    apply homset_property.

  Lemma isaprop_runitor_nat {C : tu_cat} (ru : runitor (pr2 C)) : isaprop (runitor_nat (pr1 ru)).
  Show proof.
    repeat (apply impred_isaprop ; intro).
    apply homset_property.

  Lemma bidisp_ru_disp_prebicat_is_globally_univalent : disp_univalent_2_0 bidisp_ru_disp_bicat.
  Show proof.
    apply disp_cell_unit_bicat_univalent_2_0.
    - apply bidisp_tensorunit_is_univalent_2.
    - intro ; intros.
      apply isaprop_preserves_runitor.
    - intro ; apply isaset_runitor.
    - intros C ru1 ru2 pru.
      use total2_paths_f.
      + apply funextsec ; intro.
        refine (_ @ (pr1 pru x)).
        refine (! id_left _ @ _).
        apply cancel_postcomposition.
        refine (_ @ ! id_right _).
        apply (! tensor_id _ _ _).
      + apply isaprop_runitor_nat.

  Lemma bidisp_ru_disp_prebicat_is_univalent_2 : disp_univalent_2 bidisp_ru_disp_bicat.
  Show proof.

End RightUnitorLayer.

Section UnitorsLayer.

  Definition bidisp_unitors_disp_bicat : disp_bicat tu_cat
    := disp_dirprod_bicat bidisp_lu_disp_bicat bidisp_ru_disp_bicat.

End UnitorsLayer.

Section AssociatorLayer.

  Definition disp_ass_disp_ob_mor : disp_cat_ob_mor tu_cat.
  Show proof.
    use tpair.
    - exact (λ C, associator (tu C)).
    - exact (λ C D αC αD F, preserves_associator (ftu F) αC αD).

  Definition disp_ass_disp_id_comp : disp_cat_id_comp tu_cat disp_ass_disp_ob_mor.
  Show proof.
    use tpair.
    - intros C α.
      apply id_preserves_associator.
    - intros C D E F G aC aD aE paF paG x y z.
      apply (comp_preserves_associator paF paG).

  Definition disp_ass_disp_cat_data : disp_cat_data tu_cat
    := (disp_ass_disp_ob_mor,, disp_ass_disp_id_comp).

  Definition bidisp_ass_disp_bicat : disp_bicat tu_cat
    := disp_cell_unit_bicat disp_ass_disp_cat_data.

  Lemma bidisp_ass_disp_prebicat_is_locally_univalent : disp_univalent_2_1 bidisp_ass_disp_bicat.
  Show proof.
    apply disp_cell_unit_bicat_univalent_2_1.
    intro ; intros.
    apply isaprop_preserves_associator.

  Lemma isaset_associator (C : tu_cat) : isaset (associator (pr2 C)).
  Show proof.
    apply isaset_total2.
    {
      do 3 (apply impred_isaset ; intro).
      apply homset_property.
    }
    intro.
    repeat (apply impred_isaset ; intro).
    apply isasetaprop.
    apply homset_property.

  Lemma isaprop_associator_nat (C : tu_cat) (ass : associator (pr2 C))
    : isaprop (associator_nat (pr1 ass)).
  Show proof.
    repeat (apply impred_isaprop ; intro).
    apply homset_property.

  Lemma bidisp_ass_disp_prebicat_is_globally_univalent : disp_univalent_2_0 bidisp_ass_disp_bicat.
  Show proof.
    apply disp_cell_unit_bicat_univalent_2_0.
    - apply bidisp_tensorunit_is_univalent_2.
    - intro ; intros.
      apply isaprop_preserves_associator.
    - intro ; apply isaset_associator.
    - intros C a1 a2 pa.
      use total2_paths_f.
      + apply funextsec ; intro x1 ;
          apply funextsec ; intro x2 ;
          apply funextsec ; intro x3.

        set (p := pr1 pa x1 x2 x3).
        cbn in p.
        unfold identityfunctor_preserves_tensor_data in p.
        rewrite id_right in p.
        rewrite id_right in p.
        rewrite tensor_id in p.
        rewrite id_left in p.
        rewrite tensor_id in p.
        rewrite id_right in p.
        exact p.
      + apply isaprop_associator_nat.

  Lemma bidisp_ass_disp_prebicat_is_univalent_2 : disp_univalent_2 bidisp_ass_disp_bicat.
  Show proof.

End AssociatorLayer.

Section AssociatorUnitorsLayer.

  Definition bidisp_assunitors_disp_bicat : disp_bicat tu_cat
    := disp_dirprod_bicat bidisp_unitors_disp_bicat bidisp_ass_disp_bicat.

  Definition bidisp_assunitors_disp_2cells_isaprop : disp_2cells_isaprop bidisp_assunitors_disp_bicat.
  Show proof.

  Definition bidisp_assunitors_disp_locally_groupoid : disp_locally_groupoid bidisp_assunitors_disp_bicat.
  Show proof.

  Definition bidisp_unitors_disp_prebicat_is_univalent_2
    : disp_univalent_2 bidisp_unitors_disp_bicat.
  Show proof.

  Definition bidisp_assunitors_is_disp_univalent_2
    : disp_univalent_2 bidisp_assunitors_disp_bicat.
  Show proof.

  Definition disp_tensor_unit_unitors_associator : disp_bicat bicat_of_univ_cats
    := sigma_bicat _ _ bidisp_assunitors_disp_bicat.

  Definition disp_tensor_unit_unitors_associator_is_disp_univalent_2
    : disp_univalent_2 disp_tensor_unit_unitors_associator.
  Show proof.

  Lemma disp_tensor_unit_unitors_associator_disp_2cells_isaprop
    : disp_2cells_isaprop disp_tensor_unit_unitors_associator.
  Show proof.

  Lemma disp_tensor_unit_unitors_associator_disp_locally_groupoid
    : disp_locally_groupoid disp_tensor_unit_unitors_associator.
  Show proof.
    intros C D F G α tuuaC tuuaD ptuuaC ptuuaD ptuuac.
    repeat (use tpair) ; try (exact tt).
    - apply bidisp_tensor_disp_locally_groupoid.
      apply ptuuac.
    - apply bidisp_unit_disp_locally_groupoid.
      apply ptuuac.
    - apply disp_tensor_unit_unitors_associator_disp_2cells_isaprop.
    - apply disp_tensor_unit_unitors_associator_disp_2cells_isaprop.

  Definition bidisp_assunitors_total : bicat := total_bicat disp_tensor_unit_unitors_associator.

  Definition bidisp_assunitors_is_univalent_2: is_univalent_2 bidisp_assunitors_total.
  Show proof.

  Definition assunitors_tensor (C : bidisp_assunitors_total)
    : tensor (pr1 C : univalent_category) := pr112 C.

  Definition assunitors_unit (C : bidisp_assunitors_total)
    : ob (pr1 C : univalent_category) := pr212 C.

  Definition assunitors_leftunitor (C : bidisp_assunitors_total)
    : lunitor_data (pr12 C) := pr11 (pr122 C).

  Definition assunitors_rightunitor (C : bidisp_assunitors_total)
    : runitor_data (pr12 C) := pr12 (pr122 C).

  Definition assunitors_associator (C : bidisp_assunitors_total)
    : associator_data (pr12 C) := pr1 (pr222 C).

  Definition assunitors_from_layer (C : bicat_of_univ_cats)
    : disp_tensor_unit_unitors_associator C
      -> tensor_unit_unitors_associator (C : univalent_category).
  Show proof.
    intro tuua.
    split with (pr1 tuua).
    repeat split.
    + apply (pr112 tuua).
    + apply (pr212 tuua).
    + apply (pr2 tuua).

  Definition assunitors_to_layer (C : bicat_of_univ_cats)
    : tensor_unit_unitors_associator (C : univalent_category)
      -> disp_tensor_unit_unitors_associator C.
  Show proof.
    intro tuua.
    split with (pr1 tuua).
    repeat split.
    + apply (pr12 tuua).
    + apply (pr122 tuua).
    + apply (pr222 tuua).

  Definition equality_assunitors_with_layer (C : bicat_of_univ_cats) :
    disp_tensor_unit_unitors_associator C
     tensor_unit_unitors_associator (C : univalent_category).
  Show proof.
    use weq_iso.
    - apply assunitors_from_layer.
    - apply assunitors_to_layer.
    - intro ; apply idpath.
    - intro ; apply idpath.

  Definition functor_assunitors_from_layer
             (C D : bicat_of_univ_cats) (F : bicat_of_univ_catsC,D)
             (tuuaC : disp_tensor_unit_unitors_associator C)
             (tuuaD : disp_tensor_unit_unitors_associator D)
    : tuuaC -->[F] tuuaD
      -> functor_tensor_unit_unitors_associator F
            (assunitors_from_layer C tuuaC) (assunitors_from_layer D tuuaD).
  Show proof.
    intro ptuua.
    split with (pr1 ptuua).
    repeat split.
    - apply (pr112 ptuua).
    - apply (pr212 ptuua).
    - apply (pr22 ptuua).

  Definition functor_assunitors_to_layer
             (C D : bicat_of_univ_cats) (F : bicat_of_univ_catsC,D)
             (tuuaC : disp_tensor_unit_unitors_associator C)
             (tuuaD : disp_tensor_unit_unitors_associator D)
    : functor_tensor_unit_unitors_associator F (assunitors_from_layer C tuuaC) (assunitors_from_layer D tuuaD) -> tuuaC -->[F] tuuaD.
  Show proof.
    intro ptuua.
    split with (pr1 ptuua).
    repeat split.
    - apply (pr12 ptuua).
    - apply (pr122 ptuua).
    - apply (pr222 ptuua).

  Definition equality_functor_assunitors_with_layer
             (C D : bicat_of_univ_cats) (F : bicat_of_univ_catsC,D)
             (tuuaC : disp_tensor_unit_unitors_associator C)
             (tuuaD : disp_tensor_unit_unitors_associator D)
    : tuuaC -->[F] tuuaD
             functor_tensor_unit_unitors_associator F (assunitors_from_layer C tuuaC) (assunitors_from_layer D tuuaD).
  Show proof.
    use weq_iso.
    - apply functor_assunitors_from_layer.
    - apply functor_assunitors_to_layer.
    - apply idpath.
    - apply idpath.

End AssociatorUnitorsLayer.

Module AssociatorUnitorsNotations.

  Notation "I_{ C }" := (assunitors_unit C).
  Notation "T_{ C }" := (assunitors_tensor C).
  Notation "x ⊗_{ C } y" := (tensor_on_ob T_{C} x y) (at level 31).
  Notation "f ⊗^{ C } g" := (tensor_on_hom T_{C} _ _ _ _ f g) (at level 31).

  Notation "lu^{ C }" := (assunitors_leftunitor C).
  Notation "ru^{ C }" := (assunitors_rightunitor C).
  Notation "ass^{ C }" := (assunitors_associator C).

End AssociatorUnitorsNotations.