Library UniMath.CategoryTheory.Monoidal.Actions

Generalisation of the concept of actions, over monoidal categories.
Based on the definitions in the paper "Second-Order and Dependently-Sorted Abstract Syntax" by Marcelo Fiore.

Require Import UniMath.Foundations.PartD.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.Monoidal.MonoidalCategories.
Require Import UniMath.CategoryTheory.Monoidal.MonoidalFunctors.

Local Open Scope cat.

Section A.

Context (Mon_V : monoidal_precat).

Let V := monoidal_precat_precat Mon_V.
Let I := monoidal_precat_unit Mon_V.
Let tensor := monoidal_precat_tensor Mon_V.
Notation "X ⊗ Y" := (tensor (X , Y)).
Notation "f #⊗ g" := (#tensor (f #, g)) (at level 31).
Let α' := monoidal_precat_associator Mon_V.
Let λ' := monoidal_precat_left_unitor Mon_V.
Let ρ' := monoidal_precat_right_unitor Mon_V.

Section Actions_Definition.


Section Actions_Natural_Transformations.

Context {A : precategory} (odot : functor (precategory_binproduct A V) A).

Notation "X ⊙ Y" := (odot (X , Y)) (at level 31).
Notation "f #⊙ g" := (# odot (f #, g)) (at level 31).

Definition odot_I_functor : functor A A := functor_fix_snd_arg _ _ _ odot I.

Lemma odot_I_functor_ok: functor_on_objects odot_I_functor =
  λ a, a I.
Proof.
  apply idpath.
Qed.

Definition action_right_unitor : UU := nat_iso odot_I_functor (functor_identity A).

Definition odot_x_odot_y_functor : (A V) V A :=
  functor_composite (pair_functor odot (functor_identity _)) odot.

Lemma odot_x_odot_y_functor_ok: functor_on_objects odot_x_odot_y_functor =
  λ a, (ob1 (ob1 a) ob2 (ob1 a)) ob2 a.
Proof.
  apply idpath.
Qed.

Definition odot_x_otimes_y_functor : (A V) V A :=
  functor_composite (precategory_binproduct_unassoc _ _ _)
                    (functor_composite (pair_functor (functor_identity _) tensor) odot).

Lemma odot_x_otimes_y_functor_ok: functor_on_objects odot_x_otimes_y_functor =
  λ a, ob1 (ob1 a) (ob2 (ob1 a) ob2 a).
Proof.
  apply idpath.
Qed.

Definition action_convertor : UU := nat_iso odot_x_odot_y_functor odot_x_otimes_y_functor.

Definition action_triangle_eq (ϱ : action_right_unitor) (χ : action_convertor) := (a : A), (x : V),
  (pr1 ϱ a) #⊙ (id x) = (pr1 χ ((a, I), x)) · (id a) #⊙ (pr1 λ' x).

Definition action_pentagon_eq (χ : action_convertor) := (a : A), (x y z : V),
  (pr1 χ ((a x, y), z)) · (pr1 χ ((a, x), y z)) =
  (pr1 χ ((a, x), y)) #⊙ (id z) · (pr1 χ ((a, x y), z)) ·
                                  (id a) #⊙ (pr1 α' ((x, y), z)).

End Actions_Natural_Transformations.

Definition action : UU := A : precategory, (odot : A V A), (ϱ : action_right_unitor odot), (χ : action_convertor odot), (action_triangle_eq odot ϱ χ) × (action_pentagon_eq odot χ).

Definition action_struct : UU := A : precategory, (odot : A V A), (ϱ : action_right_unitor odot), (χ : action_convertor odot), unit.

End Actions_Definition.

Definition tensorial_action : action.
Proof.
   V.
   tensor.
   ρ'.
   α'.
  exact (monoidal_precat_eq Mon_V).
Defined.

Section Strong_Monoidal_Functor_Action.

Context (Mon_A : monoidal_precat).

Let A := monoidal_precat_precat Mon_A.
Let I_A := monoidal_precat_unit Mon_A.
Let tensor_A := monoidal_precat_tensor Mon_A.
Notation "X ⊗_A Y" := (tensor_A (X , Y)) (at level 31).
Notation "f #⊗_A g" := (#tensor_A (f #, g)) (at level 31).
Let α_A := monoidal_precat_associator Mon_A.
Let λ_A := monoidal_precat_left_unitor Mon_A.
Let ρ_A := monoidal_precat_right_unitor Mon_A.

Context (U : strong_monoidal_functor Mon_V Mon_A).

Definition otimes_U_functor : A V A := functor_composite (pair_functor (functor_identity _) U) tensor_A.

Lemma otimes_U_functor_ok: functor_on_objects otimes_U_functor =
  λ av, ob1 av _A U (ob2 av).
Proof.
  apply idpath.
Qed.

Definition U_action_ρ_nat_trans : odot_I_functor otimes_U_functor functor_identity A.
  refine (nat_trans_comp _ _ _ _ (pr1 ρ_A)).
  unfold odot_I_functor.
  pose (ϵ_inv := inv_from_iso (make_iso _ (pr1 (pr2 U)))).
  set (aux := nat_trans_from_functor_fix_snd_morphism_arg _ _ _ tensor_A _ _ ϵ_inv).
  use tpair.
  - intro a.
    apply (pr1 aux a).
  - cbn; red.
    intros a a' f.
    cbn.
    rewrite functor_id.
    exact (pr2 aux a a' f).
Defined.

Lemma U_action_ρ_nat_trans_ok: nat_trans_data_from_nat_trans U_action_ρ_nat_trans =
 let ϵ_inv := inv_from_iso (make_iso _ (pr1 (pr2 U))) in λ x, id x #⊗_A ϵ_inv · pr1 ρ_A x.
Proof.
  apply idpath.
Qed.

Definition U_action_ρ_is_nat_iso : is_nat_iso U_action_ρ_nat_trans.
Proof.
  intro.
  cbn.
  use is_iso_comp_of_is_isos.
  - use is_iso_tensor_iso.
    + exact (identity_is_iso _ _).
    + use is_iso_inv_from_iso.
  - exact (pr2 ρ_A c).
Qed.

Definition U_action_ρ : action_right_unitor otimes_U_functor := make_nat_iso _ _ U_action_ρ_nat_trans U_action_ρ_is_nat_iso.

Definition U_action_χ_nat_trans : odot_x_odot_y_functor otimes_U_functor odot_x_otimes_y_functor otimes_U_functor.
Proof.
  apply (nat_trans_comp _ _ _ (pre_whisker (pair_functor (pair_functor (functor_identity _) U) U) (pr1 α_A))).
  pose (μ := pr1 (pr2 (pr2 (pr1 U)))).
  exact (pre_whisker (precategory_binproduct_unassoc _ _ _) (post_whisker_fst_param μ tensor_A)).
Defined.

Lemma U_action_χ_nat_trans_ok: nat_trans_data_from_nat_trans U_action_χ_nat_trans =
  let μ := pr1 (pr2 (pr2 (pr1 U))) in
  λ x, let k := ob1 (ob1 x) in
       let k' := ob2 (ob1 x) in
       let k'' := ob2 x in
       pr1 α_A ((k, U k'), U k'') · id k #⊗_A pr1 μ (k', k'').
Proof.
  apply idpath.
Qed.

Lemma U_action_χ_is_nat_iso : is_nat_iso U_action_χ_nat_trans.
Proof.
  intro x.
  pose (k := ob1 (ob1 x)); pose (k' := ob2 (ob1 x)); pose (k'' := ob2 x).
  use is_iso_comp_of_is_isos.
  - exact (pr2 α_A ((k, U k'), U k'')).
  - use is_iso_tensor_iso.
    + use identity_is_iso.
    + exact (pr2 (pr2 U) (k', k'')).
Qed.

Definition U_action_χ : action_convertor otimes_U_functor :=
  make_nat_iso _ _ U_action_χ_nat_trans U_action_χ_is_nat_iso.

Definition U_action_struct : action_struct.
Proof.
   A.
   otimes_U_functor.
   U_action_ρ.
   U_action_χ.
  exact tt.
Defined.

Context
  {U_action_tlaw : action_triangle_eq (A := pr1 U_action_struct)
                                      (pr1 (pr2 U_action_struct))
                                      (pr1 (pr2 (pr2 U_action_struct)))
                                      (pr1 (pr2 (pr2 (pr2 U_action_struct))))}
  {U_action_plaw : action_pentagon_eq (A := pr1 U_action_struct)
                                      (pr1 (pr2 U_action_struct))
                                      (pr1 (pr2 (pr2 (pr2 U_action_struct))))}.

Definition U_action : action.
   (pr1 U_action_struct).
   (pr1 (pr2 U_action_struct)).
   (pr1 (pr2 (pr2 U_action_struct))).
   (pr1 (pr2 (pr2 (pr2 U_action_struct)))).
   U_action_tlaw.
  exact U_action_plaw.
Defined.

End Strong_Monoidal_Functor_Action.

End A.