Lemma lineator_laxlaws_from_commutator: lineator_laxlaws Mon_W ActW ActW FF lineator_data_from_commutator. Proof. assert (γ_nat := relativelaxcommutator_ldnat γ). do 2 red in γ_nat. cbn in γ_nat. repeat split; red; intros; unfold lineator_data_from_commutator; try unfold reindexed_actor_data; try unfold reindexed_action_unitor_data; cbn; try unfold reindexed_actor_data; try unfold reindexed_action_unitor_data; cbn. - etrans. { repeat rewrite assoc. do 2 apply cancel_postcomposition. apply actorinv_nat_leftwhisker. } etrans. 2: { repeat rewrite assoc'. do 2 apply maponpaths. apply pathsinv0, actegory_actornatleft. } repeat rewrite assoc'. apply maponpaths. repeat rewrite assoc. apply cancel_postcomposition. apply pathsinv0, (bifunctor_equalwhiskers ActV). - etrans. { repeat rewrite assoc. do 2 apply cancel_postcomposition. apply actorinv_nat_rightwhisker. } etrans. 2: { repeat rewrite assoc'. do 2 apply maponpaths. apply pathsinv0, actegory_actornatleftright. } repeat rewrite assoc'. apply maponpaths. repeat rewrite assoc. apply cancel_postcomposition. etrans. { apply pathsinv0, (functor_comp (rightwhiskering_functor ActV x)). } etrans. 2: { apply (functor_comp (rightwhiskering_functor ActV x)). } apply maponpaths. apply γ_nat. - etrans. { apply maponpaths. apply (functor_comp (leftwhiskering_functor ActV v0)). } cbn. etrans. { repeat rewrite assoc. apply cancel_postcomposition. repeat rewrite assoc'. do 2 apply maponpaths. apply actegory_actornatleftright. } etrans. { repeat rewrite assoc. do 2 apply cancel_postcomposition. repeat rewrite assoc'. apply maponpaths. apply pathsinv0, (functor_comp (rightwhiskering_functor ActV x)). } cbn. etrans. { do 2 apply cancel_postcomposition. do 2 apply maponpaths. rewrite (relativelaxcommutator_ldtensor γ). repeat rewrite assoc'. do 6 apply maponpaths. etrans. { apply pathsinv0, (functor_comp (leftwhiskering_functor Mon_V v0)). } apply (functor_id_id _ _ (leftwhiskering_functor Mon_V v0)). apply (pr2 (fmonoidal_preservestensorstrongly U v w)). } rewrite id_right. etrans. { do 2 apply cancel_postcomposition. etrans. { apply maponpaths. apply (functor_comp (rightwhiskering_functor ActV x)). } cbn. rewrite assoc. apply cancel_postcomposition. apply pathsinv0, actorinv_nat_rightwhisker. } repeat rewrite assoc'. apply maponpaths. apply (z_iso_inv_on_right _ _ _ (z_iso_from_actor_iso Mon_V ActV _ _ _)). etrans. { apply cancel_postcomposition. repeat rewrite assoc. apply (functor_comp (rightwhiskering_functor ActV x)). } cbn. etrans. { rewrite assoc'. apply maponpaths. rewrite assoc. apply actegory_pentagonidentity. } repeat rewrite assoc. apply cancel_postcomposition. rewrite <- actegory_pentagonidentity. etrans. { apply cancel_postcomposition. repeat rewrite assoc'. apply (functor_comp (rightwhiskering_functor ActV x)). } cbn. repeat rewrite assoc'. apply maponpaths. etrans. 2: { apply maponpaths. etrans. 2: { apply maponpaths. apply cancel_postcomposition. apply pathsinv0, (functor_comp (leftwhiskering_functor ActV (F v))). } cbn. repeat rewrite assoc. do 3 apply cancel_postcomposition. etrans. 2: { apply (functor_comp (leftwhiskering_functor ActV (F v))). } apply pathsinv0, (functor_id_id _ _ (leftwhiskering_functor ActV (F v))). apply (pr1 (actegory_actorisolaw Mon_V ActV _ _ _)). } rewrite id_left. etrans. 2: { apply maponpaths. rewrite assoc'. apply cancel_postcomposition. apply pathsinv0, (functor_comp (leftwhiskering_functor ActV (F v))). } cbn. etrans. 2: { repeat rewrite assoc. do 3 apply cancel_postcomposition. apply pathsinv0, actegory_actornatleftright. } etrans. { apply cancel_postcomposition. apply (functor_comp (rightwhiskering_functor ActV x)). } cbn. repeat rewrite assoc'. apply maponpaths. etrans. { apply cancel_postcomposition. apply (functor_comp (rightwhiskering_functor ActV x)). } cbn. etrans. { rewrite assoc'. apply maponpaths. apply pathsinv0, actegory_actornatright. } repeat rewrite assoc. apply cancel_postcomposition. apply (z_iso_inv_on_left _ _ _ _ (z_iso_from_actor_iso Mon_V ActV _ _ _)). cbn. rewrite assoc'. rewrite <- actegory_pentagonidentity. etrans. 2: { repeat rewrite assoc. do 2 apply cancel_postcomposition. etrans. 2: { apply (functor_comp (rightwhiskering_functor ActV x)). } apply pathsinv0, (functor_id_id _ _ (rightwhiskering_functor ActV x)). apply (pr2 (monoidal_associatorisolaw Mon_V _ _ _)). } rewrite id_left. apply idpath. - etrans. { apply maponpaths. apply (functor_comp (leftwhiskering_functor ActV v0)). } cbn. etrans. { repeat rewrite assoc. apply cancel_postcomposition. repeat rewrite assoc'. do 2 apply maponpaths. apply actegory_actornatleftright. } etrans. { repeat rewrite assoc. do 2 apply cancel_postcomposition. repeat rewrite assoc'. apply maponpaths. apply pathsinv0, (functor_comp (rightwhiskering_functor ActV x)). } cbn. etrans. { do 2 apply cancel_postcomposition. do 2 apply maponpaths. rewrite (relativelaxcommutator_ldunit γ). repeat rewrite assoc'. do 3 apply maponpaths. etrans. { apply pathsinv0, (functor_comp (leftwhiskering_functor Mon_V v0)). } apply (functor_id_id _ _ (leftwhiskering_functor Mon_V v0)). apply (pr2 (fmonoidal_preservesunitstrongly U)). } rewrite id_right. etrans. { do 2 apply cancel_postcomposition. etrans. { apply maponpaths. apply (functor_comp (rightwhiskering_functor ActV x)). } cbn. rewrite assoc. apply cancel_postcomposition. apply pathsinv0, actorinv_nat_rightwhisker. } repeat rewrite assoc'. apply maponpaths. etrans. { repeat rewrite assoc'. do 2 apply maponpaths. apply actegory_triangleidentity. } etrans. { apply maponpaths. apply pathsinv0, (functor_comp (rightwhiskering_functor ActV x)). } cbn. rewrite assoc'. rewrite (pr2 (monoidal_rightunitorisolaw Mon_V v0)). rewrite id_right. rewrite <- actegory_triangleidentity'. rewrite assoc. rewrite (pr2 (actegory_actorisolaw Mon_V ActV _ _ _)). apply id_left. 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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.CategoryTheory.Actegories.ConstructionOfActegories. Require Import UniMath.CategoryTheory.coslicecat. Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Actegories.CoproductsInActegories. Require Import UniMath.CategoryTheory.Actegories.ProductsInActegories. Require Import UniMath.CategoryTheory.Actegories.ProductActegory. Import BifunctorNotations. Import MonoidalNotations. Import ActegoryNotations. Section ActegoryMorphismFromRelativeLaxCommutator. End ActegoryMorphismFromRelativeLaxCommutator.