Library UniMath.CategoryTheory.Monoidal.Displayed.MonoidalSections

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.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal.
Require Import UniMath.CategoryTheory.Monoidal.Functors.
Require Import UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.

Local Open Scope cat.
Local Open Scope mor_disp_scope.

Section MonoidalSections.

  Import BifunctorNotations.
  Import MonoidalNotations.
  Import DisplayedBifunctorNotations.
  Import DisplayedMonoidalNotations.

  Context {C : category} {D : disp_cat C}.
  Let TD : category := total_category D.
  Context (M : monoidal C) (DM : disp_monoidal D M).
  Let TM : monoidal TD := total_monoidal DM.

  Definition section_preserves_tensor_data (sd : section_disp D) : UU
    := ∏ (x y : C), sd x ⊗⊗_{DM} sd y -->[identity (x ⊗_{M} y)] sd (x ⊗_{M} y).

  Lemma sectionfunctor_preserves_tensordata
        {sd : section_disp D}
        (spt : section_preserves_tensor_data sd)
    : preserves_tensordata M TM (section_functor sd).
  Show proof.
    intros x y.
    use tpair.
    - apply identity.
    - apply spt.

  Definition section_preserves_unit (sd : section_disp D) : UU
    := dI_{DM} -->[identity I_{M}] sd I_{M}.

  Lemma sectionfunctor_preserves_unit
        {sd : section_disp D}
        (spu : section_preserves_unit sd)
    : preserves_unit M TM (section_functor sd).
  Show proof.
    use tpair.
    - apply identity.
    - apply spu.

  Definition smonoidal_data (sd : section_disp D) : UU
    := (section_preserves_tensor_data sd) × (section_preserves_unit sd).
  Definition smonoidal_preserves_tensor {sd : section_disp D} (ms : smonoidal_data sd)
    : section_preserves_tensor_data sd := pr1 ms.
  Definition smonoidal_preserves_unit {sd : section_disp D} (ms : smonoidal_data sd)
    : section_preserves_unit sd := pr2 ms.

  Definition sectionfunctor_fmonoidal_data
             {sd : section_disp D}
             (spt : section_preserves_tensor_data sd)
             (spu : section_preserves_unit sd)
    : fmonoidal_data M TM (section_functor sd)
    := (sectionfunctor_preserves_tensordata spt,,sectionfunctor_preserves_unit spu).

  Notation "# F" := (section_disp_on_morphisms F) (at level 3) : mor_disp_scope.

  Definition section_preserves_tensor_nat_left
             {sd : section_disp D}
             (spt : section_preserves_tensor_data sd)
    : UU
    := ∏ (x y1 y2 : C) (g : C⟦y1,y2⟧),
       (sd x ⊗⊗^{DM}_{l} #sd g) ;; spt x y2
       =
       transportb
         _
         (id_right (x ⊗^{M}_{l} g) @ pathsinv0 (id_left (x ⊗^{M}_{l} g)))
         (spt x y1 ;; #sd (x ⊗^{M}_{l} g)).

  Lemma sectionfunctor_preserves_tensor_nat_left
        {sd : section_disp D}
        {spt : section_preserves_tensor_data sd}
        (sptnl : section_preserves_tensor_nat_left spt)
    : preserves_tensor_nat_left (sectionfunctor_preserves_tensordata spt).
  Show proof.
    intros x y1 y2 g.
    use total2_paths_b.
    - cbn.
      rewrite id_left.
      apply id_right.
    - cbn.
      rewrite sptnl.
      apply transportb_transpose_left.
      rewrite transport_f_b.
      apply pathsinv0.
      apply transportf_set.
      apply homset_property.

  Definition section_preserves_tensor_nat_right
             {sd : section_disp D}
             (spt : section_preserves_tensor_data sd)
    : UU
    := ∏ (x1 x2 y : C) (f : C⟦x1,x2⟧),
       (#sd f ⊗⊗^{DM}_{r} sd y) ;; spt x2 y
       =
       transportb
         _
         (id_right (f ⊗^{M}_{r} y) @ pathsinv0 (id_left (f ⊗^{M}_{r} y)))
         (spt x1 y ;; #sd (f ⊗^{M}_{r} y)).

  Lemma sectionfunctor_preserves_tensor_nat_right
        {sd : section_disp D}
        {spt : section_preserves_tensor_data sd}
        (sptnl : section_preserves_tensor_nat_right spt)
    : preserves_tensor_nat_right (sectionfunctor_preserves_tensordata spt).
  Show proof.
    intros x1 x2 y f.
    use total2_paths_b.
    - cbn.
      rewrite id_left.
      apply id_right.
    - cbn.
      rewrite sptnl.
      apply transportb_transpose_left.
      rewrite transport_f_b.
      apply pathsinv0.
      apply transportf_set.
      apply homset_property.

  Definition equality_for_leftunitality
             (x : C)
    : identity I_{M} ⊗^{M}_{r} x · identity (I_{M} ⊗_{M} x) · lu^{M}_{x}
      =
      lu^{M}_{x}.
  Show proof.
    rewrite assoc'.
    rewrite (bifunctor_rightid M).
    rewrite id_left.
    apply id_left.

  Definition section_preserves_leftunitality
             {sd : section_disp D}
             (spt : section_preserves_tensor_data sd)
             (spu : section_preserves_unit sd)
    : UU
    := ∏ (x : C),
       spu ⊗⊗^{DM}_{r} sd x ;; spt I_{M} x ;; # sd lu^{M}_{x}
       =
       transportb
         _
         (equality_for_leftunitality x)
         (dlu^{DM}_{sd x}).

  Definition sectionfunctor_preserves_leftunitality
             {sd : section_disp D}
             {spt : section_preserves_tensor_data sd}
             {spu : section_preserves_unit sd}
             (splu : section_preserves_leftunitality spt spu)
    : preserves_leftunitality
        (sectionfunctor_preserves_tensordata spt)
        (sectionfunctor_preserves_unit spu).
  Show proof.
    intro x.
    use total2_paths_b.
    - cbn.
      rewrite assoc'.
      rewrite (bifunctor_rightid M).
      rewrite id_left.
      apply id_left.
    - cbn.
      rewrite splu.
      apply transportb_transpose_left.
      rewrite transport_f_b.
      apply pathsinv0.
      apply transportf_set.
      apply homset_property.

  Definition equality_for_rightunitality (x : C)
    : x ⊗^{M}_{l} identity I_{M} · identity (x ⊗_{M} I_{M}) · ru^{M}_{x}
      =
      ru^{M}_{x}.
  Show proof.
    rewrite assoc'.
    rewrite (bifunctor_leftid M).
    rewrite id_left.
    apply id_left.

  Definition section_preserves_rightunitality
             {sd : section_disp D}
             (spt : section_preserves_tensor_data sd)
             (spu : section_preserves_unit sd)
    : UU
    := ∏ (x : C),
       sd x ⊗⊗^{DM}_{l} spu ;; spt x I_{M} ;; # sd ru^{M}_{x}
       =
       transportb
         _
         (equality_for_rightunitality x)
         (dru^{DM}_{sd x}).

  Definition sectionfunctor_preserves_rightunitality
             {sd : section_disp D}
             {spt : section_preserves_tensor_data sd}
             {spu : section_preserves_unit sd}
             (spru : section_preserves_rightunitality spt spu)
    : preserves_rightunitality
        (sectionfunctor_preserves_tensordata spt)
        (sectionfunctor_preserves_unit spu).
  Show proof.
    intro x.
    use total2_paths_b.
    - cbn.
      rewrite assoc'.
      rewrite (bifunctor_leftid M).
      rewrite id_left.
      apply id_left.
    - cbn.
      rewrite spru.
      apply transportb_transpose_left.
      rewrite transport_f_b.
      apply pathsinv0.
      apply transportf_set.
      apply homset_property.

  Definition equality_for_associativity
             (x y z : C)
    : identity (x ⊗_{M} y) ⊗^{M}_{r} z · identity ((x ⊗_{M} y) ⊗_{M} z) · α^{M}_{ x, y, z}
      =
      α^{M}_{ x, y, z} · x ⊗^{M}_{l} identity (y ⊗_{M} z) · identity (x ⊗_{M} (y ⊗_{M} z)).
  Show proof.
    rewrite assoc'.
    rewrite (bifunctor_leftid M).
    rewrite id_left.
    rewrite id_right.
    rewrite id_right.
    rewrite (bifunctor_rightid M).
    apply id_left.

  Definition section_preserves_associativity
             {sd : section_disp D}
             (spt : section_preserves_tensor_data sd)
    : UU
    := ∏ (x y z : C),
       spt x y ⊗⊗^{DM}_{r} sd z ;; spt (x ⊗_{M} y) z ;; # sd α^{M}_{ x, y, z}
       =
       transportb
         _
         (equality_for_associativity x y z)
         (dα^{DM}_{ sd x, sd y, sd z} ;; sd x ⊗⊗^{DM}_{l} spt y z ;; spt x (y ⊗_{M} z)).

  Definition sectionfunctor_preserves_associativity
             {sd : section_disp D}
             {spt : section_preserves_tensor_data sd}
             (spa : section_preserves_associativity spt)
    : preserves_associativity (sectionfunctor_preserves_tensordata spt).
  Show proof.
    intros x y z.
    use total2_paths_b.
    - cbn.
      rewrite assoc'.
      rewrite (bifunctor_leftid M).
      rewrite id_right.
      rewrite id_right.
      rewrite id_left.
      rewrite (bifunctor_rightid M).
      apply id_left.
    - cbn.
      rewrite spa.
      apply transportb_transpose_left.
      rewrite transport_f_b.
      apply pathsinv0.
      apply transportf_set.
      apply homset_property.

  Definition smonoidal_laxlaws {sd : section_disp D} (ms : smonoidal_data sd) : UU
    := (section_preserves_tensor_nat_left
          (smonoidal_preserves_tensor ms))
       × (section_preserves_tensor_nat_right
            (smonoidal_preserves_tensor ms))
       × (section_preserves_associativity
            (smonoidal_preserves_tensor ms))
       × (section_preserves_leftunitality
            (smonoidal_preserves_tensor ms)
            (smonoidal_preserves_unit ms))
       × (section_preserves_rightunitality
            (smonoidal_preserves_tensor ms)
            (smonoidal_preserves_unit ms)).

  Definition smonoidal_preserves_tensornatleft
             {sd : section_disp D}
             {ms : smonoidal_data sd}
             (msl : smonoidal_laxlaws ms)
    : section_preserves_tensor_nat_left (smonoidal_preserves_tensor ms)
    := pr1 msl.

  Definition smonoidal_preserves_tensornatright
             {sd : section_disp D}
             {ms : smonoidal_data sd}
             (msl : smonoidal_laxlaws ms)
    : section_preserves_tensor_nat_right (smonoidal_preserves_tensor ms)
    := pr1 (pr2 msl).

  Definition smonoidal_preserves_associativity
             {sd : section_disp D}
             {ms : smonoidal_data sd}
             (msl : smonoidal_laxlaws ms)
    : section_preserves_associativity (smonoidal_preserves_tensor ms)
    := pr1 (pr2 (pr2 msl)).

  Definition smonoidal_preserves_leftunitality
             {sd : section_disp D}
             {ms : smonoidal_data sd}
             (msl : smonoidal_laxlaws ms)
    : section_preserves_leftunitality
        (smonoidal_preserves_tensor ms)
        (smonoidal_preserves_unit ms)
    := pr1 (pr2 (pr2 (pr2 msl))).

  Definition smonoidal_preserves_rightunitality
             {sd : section_disp D}
             {ms : smonoidal_data sd}
             (msl : smonoidal_laxlaws ms)
    : section_preserves_rightunitality
        (smonoidal_preserves_tensor ms)
        (smonoidal_preserves_unit ms)
    := pr2 (pr2 (pr2 (pr2 msl))).

  Definition smonoidal_lax (sd : section_disp D) : UU
    := ∑ (ms : smonoidal_data sd), smonoidal_laxlaws ms.

  Definition smonoidal_sdata
             {sd : section_disp D}
             (sm : smonoidal_lax sd)
    : smonoidal_data sd := pr1 sm.

  Coercion smonoidal_sdata : smonoidal_lax >-> smonoidal_data.

  Definition smonoidal_slaxlaws
             {sd : section_disp D}
             (sm : smonoidal_lax sd)
    : smonoidal_laxlaws sm
    := pr2 sm.

  Definition sectionfunctor_fmonoidal_laxlaws
             {sd : section_disp D}
             {ms : smonoidal_data sd}
             (ml : smonoidal_laxlaws ms)
    : fmonoidal_laxlaws
        (sectionfunctor_fmonoidal_data
           (smonoidal_preserves_tensor ms)
           (smonoidal_preserves_unit ms))
    := (sectionfunctor_preserves_tensor_nat_left (smonoidal_preserves_tensornatleft ml),,
        sectionfunctor_preserves_tensor_nat_right (smonoidal_preserves_tensornatright ml),,
        sectionfunctor_preserves_associativity (smonoidal_preserves_associativity ml),,
        sectionfunctor_preserves_leftunitality (smonoidal_preserves_leftunitality ml),,
        sectionfunctor_preserves_rightunitality (smonoidal_preserves_rightunitality ml)).

  Definition sectionfunctor_fmonoidal_lax
             {sd : section_disp D}
             (ms : smonoidal_lax sd)
    : fmonoidal_lax M TM (section_functor sd)
    := (sectionfunctor_fmonoidal_data
          (smonoidal_preserves_tensor ms)
          (smonoidal_preserves_unit ms)
        ,,
        sectionfunctor_fmonoidal_laxlaws (smonoidal_slaxlaws ms)).

  Definition smonoidal_strongtensor
             {sd : section_disp D}
             (spt : section_preserves_tensor_data sd)
    : UU
    := ∏ (x y : C),
       is_z_iso_disp
         (identity_z_iso (x⊗_{M} y))
         (spt x y).

  Definition smonoidal_strongunit
             {sd : section_disp D}
             (spu : section_preserves_unit sd)
    : UU
    := is_z_iso_disp
         (identity_z_iso (I_{M}))
         spu.

  Definition smonoidal_stronglaws
             {sd : section_disp D}
             (ms : smonoidal_data sd)
    : UU
    := smonoidal_strongtensor (smonoidal_preserves_tensor ms)
       ×
       smonoidal_strongunit (smonoidal_preserves_unit ms).

  Definition smonoidal (sd : section_disp D) : UU
    := ∑ (ms : smonoidal_lax sd), smonoidal_stronglaws ms.

  Definition smonoidal_smonoidallax
             {sd : section_disp D}
             (sm : smonoidal sd)
    : smonoidal_lax sd
    := pr1 sm.
  Coercion smonoidal_smonoidallax : smonoidal >-> smonoidal_lax.

  Definition smonoidal_smonoidalstronglaws
             {sd : section_disp D}
             (sm : smonoidal sd)
    : smonoidal_stronglaws sm
    := pr2 sm.

  Definition smonoidal_smonoidalstrongtensor
             {sd : section_disp D}
             (sm : smonoidal sd)
    : smonoidal_strongtensor (smonoidal_preserves_tensor sm)
    := pr1 (smonoidal_smonoidalstronglaws sm).

  Definition smonoidal_smonoidalstrongunit
             {sd : section_disp D}
             (sm : smonoidal sd)
    : smonoidal_strongunit (smonoidal_preserves_unit sm)
    := pr2 (smonoidal_smonoidalstronglaws sm).

  Definition sectionfunctor_preservestensorstrongly
             {sd : section_disp D}
             {ms : smonoidal sd}
             (pfstrong : smonoidal_strongtensor (smonoidal_preserves_tensor ms))
    : preserves_tensor_strongly
        (sectionfunctor_preserves_tensordata
           (smonoidal_preserves_tensor ms)).
  Show proof.
    intros x y.
    use tpair.
    - use tpair.
      + apply identity.
      + exact (pr1 (pfstrong x y)).
    - use tpair.
      + use total2_paths_b.
        * apply id_left.
        * apply (pr2 (pr2 (pfstrong x y))).
      + use total2_paths_b.
        * apply id_left.
        * apply (pr1 (pr2 (pfstrong x y))).

  Definition sectionfunctor_preservesunitstrongly
             {sd : section_disp D}
             {ms : smonoidal sd}
             (pfstrong : smonoidal_strongunit (smonoidal_preserves_unit ms))
    : preserves_unit_strongly
        (sectionfunctor_preserves_unit (smonoidal_preserves_unit ms)).
  Show proof.
    use tpair.
    - use tpair.
      + apply identity.
      + exact (pr1 pfstrong).
    - use tpair.
      + use total2_paths_b.
        * apply id_left.
        * apply (pr22 pfstrong).
      + use total2_paths_b.
        * apply id_left.
        * apply (pr1 (pr2 pfstrong)).

  Definition sectionfunctor_fmonoidal
             {sd : section_disp D}
             (ms : smonoidal sd)
    : fmonoidal M TM (section_functor sd)
    := (sectionfunctor_fmonoidal_lax ms ,,
        sectionfunctor_preservestensorstrongly (smonoidal_smonoidalstrongtensor ms) ,,
        sectionfunctor_preservesunitstrongly (smonoidal_smonoidalstrongunit ms)).
End MonoidalSections.