Lemma reindexed_actegory_laws: actegory_laws Mon_W reindexed_actegory_data. Proof. split5. - exact reindexed_action_data_is_bifunctor. - split3. + intros x y f. cbn. unfold reindexed_action_unitor_data. etrans. 2: { rewrite assoc'. apply maponpaths. exact (actegory_unitornat Mon_V Act x y f). } do 2 rewrite assoc. apply maponpaths_2. apply (! bifunctor_equalwhiskers Act _ _ _ _ (pr1 (fmonoidal_preservesunitstrongly U)) f). + cbn. unfold reindexed_action_unitor_data. unfold reindexed_action_unitorinv_data. etrans. { rewrite assoc'. apply maponpaths. rewrite assoc. apply maponpaths_2. exact (pr1 (actegory_unitorisolaw Mon_V Act x)). } rewrite id_left. refine (! bifunctor_rightcomp Act _ _ _ _ _ _ @ _). etrans. { apply maponpaths. exact (pr22 (fmonoidal_preservesunitstrongly U)). } apply (bifunctor_rightid Act). + cbn. unfold reindexed_action_unitor_data. unfold reindexed_action_unitorinv_data. etrans. { rewrite assoc'. apply maponpaths. rewrite assoc. apply maponpaths_2. refine (! bifunctor_rightcomp Act _ _ _ _ _ _ @ _). apply maponpaths. exact (pr12 (fmonoidal_preservesunitstrongly U)). } rewrite bifunctor_rightid. rewrite id_left. exact (pr2 (actegory_unitorisolaw Mon_V Act x)). - split4. + intros v w z z' h. cbn. unfold reindexed_actor_data. rewrite assoc'. rewrite (actegory_actornatleft Mon_V Act (F v) (F w) z z' h). do 2 rewrite assoc. apply maponpaths_2. apply (bifunctor_equalwhiskers Act). + intros v v' w z f. cbn. unfold reindexed_actor_data. rewrite assoc'. rewrite (actegory_actornatright Mon_V Act). do 2 rewrite assoc. apply maponpaths_2. do 2 rewrite (! bifunctor_rightcomp Act _ _ _ _ _ _). apply maponpaths. apply preserves_tensorinv_nat_right. exact (fmonoidal_preservestensornatright U). + intros v w w' z g. cbn. unfold reindexed_actor_data. rewrite assoc'. rewrite (actegory_actornatleftright Mon_V Act). do 2 rewrite assoc. apply maponpaths_2. do 2 rewrite (! bifunctor_rightcomp Act _ _ _ _ _ _). apply maponpaths. apply preserves_tensorinv_nat_left. exact (fmonoidal_preservestensornatleft U). + split. * cbn. unfold reindexed_actor_data. unfold reindexed_actorinv_data. etrans. { rewrite assoc'. apply maponpaths. rewrite assoc. apply maponpaths_2. exact (pr1 (actegory_actorisolaw Mon_V Act (F v) (F w) z)). } rewrite id_left. refine (! bifunctor_rightcomp Act _ _ _ _ _ _ @ _). etrans. { apply maponpaths. exact (pr22 (fmonoidal_preservestensorstrongly U v w)). } apply bifunctor_rightid. * cbn. unfold reindexed_actor_data. unfold reindexed_actorinv_data. etrans. { rewrite assoc'. apply maponpaths. rewrite assoc. apply maponpaths_2. refine (! bifunctor_rightcomp Act _ _ _ _ _ _ @ _). apply maponpaths. exact (pr12 (fmonoidal_preservestensorstrongly U v w)). } rewrite bifunctor_rightid. rewrite id_left. exact (pr2 (actegory_actorisolaw Mon_V Act (F v) (F w) z)). - intros v y. cbn. unfold reindexed_actor_data. unfold reindexed_action_unitor_data. rewrite assoc'. rewrite (bifunctor_leftcomp Act). etrans. { apply maponpaths. rewrite assoc. apply maponpaths_2. apply (actegory_actornatleftright Mon_V Act). } rewrite assoc'. etrans. { do 2 apply maponpaths. apply (actegory_triangleidentity Mon_V Act (F v) y). } do 2 rewrite (! bifunctor_rightcomp Act _ _ _ _ _ _). apply maponpaths. rewrite (! fmonoidal_preservesrightunitality U v). etrans. { apply maponpaths. rewrite assoc. apply maponpaths_2. rewrite assoc. apply maponpaths_2. rewrite (! bifunctor_leftcomp Mon_V _ _ _ _ _ _). apply maponpaths. exact (pr22 (fmonoidal_preservesunitstrongly U)). } rewrite bifunctor_leftid. rewrite id_left. rewrite assoc. rewrite (pr22 (fmonoidal_preservestensorstrongly U v I_{Mon_W})). apply id_left. - intros w v v' z. cbn. unfold reindexed_actor_data. etrans. 2: { rewrite assoc. apply maponpaths_2. rewrite assoc'. apply maponpaths. exact (! actegory_actornatright Mon_V Act _ _ _ _ _). } etrans. 2: { rewrite assoc'. apply maponpaths. rewrite assoc'. apply maponpaths. exact (actegory_pentagonidentity Mon_V Act (F w) (F v) (F v') z). } rewrite (bifunctor_leftcomp Act). rewrite assoc'. etrans. { apply maponpaths. rewrite assoc. apply maponpaths_2. rewrite assoc'. apply maponpaths. apply (actegory_actornatleftright Mon_V Act). } repeat (rewrite assoc). do 2 apply maponpaths_2. repeat (rewrite (! bifunctor_rightcomp Act _ _ _ _ _ _)). apply maponpaths. set (pα := fmonoidal_preservesassociativity U). apply (! preserves_associativity_of_inverse_preserves_tensor pα _ _ _ _). Qed.
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.Functors. Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects. Require Import UniMath.CategoryTheory.Actegories.Actegories. Import BifunctorNotations. Import MonoidalNotations. Import ActegoryNotations.