Lemma inner_swap_hexagon (x1 x2 y1 y2 z1 z2 : V) : inner_swap (x1 ⊗ x2) y1 (y2 ⊗ z1) z2 · (inner_swap x1 x2 y2 z1 ⊗^{V}_{r} (y1 ⊗ z2) · mon_lassociator _ _ _) = (mon_lassociator _ _ _ #⊗ mon_lassociator _ _ _) · (inner_swap x1 (x2 ⊗ y1) y2 (z1 ⊗ z2) · (x1 ⊗ y2) ⊗^{V}_{l} inner_swap x2 y1 z1 z2). Proof. rewrite tensor_split. rewrite <- tensor_mor_left. rewrite !assoc'. set (auxiso := functor_on_z_iso (leftwhiskering_functor V (x1 ⊗ x2 ⊗ y1)) (z_iso_from_associator_iso V y2 z1 z2)). apply (z_iso_inv_to_left _ _ _ auxiso). cbn. clear auxiso. etrans. { rewrite assoc. apply maponpaths_2. assert (auxH := inner_swap_composite_third_arg (x1 ⊗ x2) y1 y2 z1 z2). rewrite <- tensor_mor_right in auxH. set (auxiso1 := functor_on_z_iso (rightwhiskering_functor V (y1 ⊗ z2)) (z_iso_from_associator_iso V (x1 ⊗ x2) y2 z1)). apply pathsinv0, (z_iso_inv_to_right _ _ _ _ auxiso1), pathsinv0 in auxH. rewrite tensor_mor_left. cbn in auxH. exact auxH. } etrans. 2: { rewrite assoc. apply maponpaths_2. assert (auxH := inner_swap_composite_second_arg x1 x2 y1 y2 (z1 ⊗ z2)). rewrite <- tensor_mor_left in auxH. set (auxiso1 := functor_on_z_iso (leftwhiskering_functor V (x1 ⊗ y2)) (z_iso_from_associator_iso V x2 y1 (z1 ⊗ z2))). apply pathsinv0, (z_iso_inv_on_left _ _ _ _ auxiso1), pathsinv0 in auxH. cbn in auxH. rewrite tensor_mor_left in auxH. exact auxH. } rewrite !assoc'. apply maponpaths. etrans. 2: { rewrite !assoc. do 2 apply maponpaths_2. assert (auxH := mon_lassociator_inner_swap x1 x2 y2 (y1 ⊗ (z1 ⊗ z2))). apply pathsinv0, (z_iso_inv_on_left _ _ _ _ (z_iso_from_associator_iso V _ _ _)), pathsinv0 in auxH. cbn in auxH. exact auxH. } etrans. { rewrite !assoc. do 3 apply maponpaths_2. assert (auxH := mon_rassociator_inner_swap ((x1 ⊗ x2) ⊗ y2) y1 z1 z2). apply pathsinv0, (z_iso_inv_to_right _ _ _ _ (z_iso_from_associator_iso V _ _ _)), pathsinv0 in auxH. cbn in auxH. exact auxH. } rewrite ! tensor_mor_left. rewrite ! tensor_mor_right. rewrite tensor_comp_id_l. rewrite tensor_comp_id_r. etrans. { apply maponpaths_2. rewrite !assoc'. do 5 apply maponpaths. etrans. { apply pathsinv0, tensor_comp_id_r. } apply maponpaths_2. assert (auxH := mon_lassociator_inner_swap x1 x2 y2 z1). apply pathsinv0, (z_iso_inv_on_left _ _ _ _ (z_iso_from_associator_iso V _ _ _)) in auxH. cbn in auxH. exact auxH. } etrans. 2: { rewrite !assoc'. do 5 apply maponpaths. etrans. 2: { apply tensor_comp_id_l. } apply maponpaths. assert (auxH := mon_rassociator_inner_swap x2 y1 z1 z2). apply pathsinv0, (z_iso_inv_to_right _ _ _ _ (z_iso_from_associator_iso V _ _ _)) in auxH. cbn in auxH. exact auxH. } change ((pr12 V) x2 y2) with (sym_mon_braiding V x2 y2). change ((pr12 V) y1 z1) with (sym_mon_braiding V y1 z1). etrans. { rewrite !assoc'. apply maponpaths. rewrite !assoc. do 4 apply maponpaths_2. apply pathsinv0, tensor_rassociator. } rewrite !assoc. rewrite <- tensor_comp_id_l. etrans. 2: { rewrite !assoc'. apply maponpaths. rewrite !assoc. do 3 apply maponpaths_2. apply tensor_lassociator. } rewrite !assoc. rewrite <- tensor_comp_id_r. rewrite !assoc'. transparent assert (auxiso : (z_iso (x1 ⊗ x2 ⊗ y2 ⊗ (y1 ⊗ (z1 ⊗ z2))) (x1 ⊗ x2 ⊗ y2 ⊗ (z1 ⊗ y1 ⊗ z2)))). { apply (functor_on_z_iso (leftwhiskering_functor V _)). use z_iso_comp. 2: { apply z_iso_inv. exact (z_iso_from_associator_iso V _ _ _). } apply (functor_on_z_iso (rightwhiskering_functor V _)). apply sym_mon_braiding_z_iso. } rewrite <- tensor_mor_left. rewrite <- tensor_mor_right. apply pathsinv0, (z_iso_inv_to_left _ _ _ auxiso), pathsinv0. cbn. clear auxiso. etrans. 2: { rewrite !assoc. do 4 apply maponpaths_2. rewrite tensor_mor_left. apply tensor_swap. } rewrite !assoc'. transparent assert (auxiso : (z_iso (x1 ⊗ x2 ⊗ y2 ⊗ (z1 ⊗ y1 ⊗ z2)) (x1 ⊗ y2 ⊗_{ pr1 V} x2 ⊗ (z1 ⊗ y1 ⊗ z2)))). { apply (functor_on_z_iso (rightwhiskering_functor V _)). use z_iso_comp. 2: { exact (z_iso_from_associator_iso V _ _ _). } apply (functor_on_z_iso (leftwhiskering_functor V _)). apply sym_mon_braiding_z_iso. } apply pathsinv0. rewrite <- tensor_mor_left. rewrite <- tensor_mor_right. apply pathsinv0, (z_iso_inv_to_left _ _ _ auxiso). cbn. clear auxiso. change ((pr12 V) x2 y2) with (sym_mon_braiding V x2 y2). change ((pr12 V) y2 x2) with (sym_mon_braiding V y2 x2). change ((pr12 V) y1 z1) with (sym_mon_braiding V y1 z1). change ((pr12 V) z1 y1) with (sym_mon_braiding V z1 y1). rewrite tensor_mor_left. rewrite !tensor_mor_right. transparent assert (middle : (V ⟦ x1 ⊗ (y2 ⊗ x2) ⊗ (z1 ⊗ y1 ⊗ z2), x1 ⊗ y2 ⊗ (x2 ⊗ z1 ⊗ (y1 ⊗ z2)) ⟧)). { refine (_ #⊗ _ · _). - apply mon_rassociator. - apply mon_lassociator. - refine (mon_lassociator _ _ _ · _). refine ((identity (x1 ⊗ y2)) #⊗ _). apply mon_rassociator. } intermediate_path middle; [| apply pathsinv0]. - rewrite tensor_comp_id_l. rewrite tensor_comp_id_r. rewrite !assoc'. match goal with | [|- ?s · _ = _ ] => set (symyx := s) end. etrans. { do 5 apply maponpaths. apply maponpaths_2. etrans. { apply maponpaths_2. apply maponpaths. rewrite assoc. apply maponpaths_2. apply pathsinv0, tensor_lassociator. } rewrite !tensor_comp_id_r. rewrite !assoc'. apply maponpaths. apply maponpaths_2. refine (!(id_right _) @ _). etrans. { apply maponpaths. apply pathsinv0, mon_lassociator_rassociator. } rewrite assoc. apply maponpaths_2. etrans. { apply tensor_lassociator. } rewrite tensor_id_id. apply maponpaths. assert (auxH := tensor_swap (identity x1 #⊗ sym_mon_braiding V x2 y2) (mon_lassociator z1 y1 z2)). do 3 rewrite <- tensor_mor_left in auxH. transparent assert (auxiso : (z_iso ((x1 ⊗ (x2 ⊗ y2)) ⊗_{ V} (z1 ⊗ y1 ⊗ z2)) ((x1 ⊗ (x2 ⊗ y2)) ⊗_{ V} (z1 ⊗ (y1 ⊗ z2))))). { apply (functor_on_z_iso (leftwhiskering_functor V _)). exact (z_iso_from_associator_iso V _ _ _). } apply (z_iso_inv_on_right _ _ _ auxiso) in auxH. cbn in auxH. clear auxiso. rewrite ! tensor_mor_left in auxH. apply (!auxH). } change ((pr12 V) x2 y2) with (sym_mon_braiding V x2 y2). rewrite !assoc. match goal with | [|- _ · ?s · _ · _ · _ · _ · _ · _ = _ ] => set (symxy := s) end. etrans. { do 7 apply maponpaths_2. rewrite !assoc'. apply maponpaths. intermediate_path (identity ((x1 ⊗ (x2 ⊗ y2)) ⊗ (z1 ⊗ y1 ⊗ z2))). - etrans. { do 3 apply maponpaths. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite tensor_lassociator. rewrite !assoc. apply maponpaths_2. apply mon_lassociator_lassociator. } etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_id_r. rewrite mon_rassociator_lassociator. rewrite tensor_id_id. rewrite id_left. apply idpath. } etrans. { apply maponpaths. rewrite !assoc. rewrite mon_rassociator_lassociator. rewrite id_left. apply idpath. } rewrite tensor_id_id. rewrite <- tensor_comp_mor. rewrite id_left, id_right. etrans. { apply maponpaths. refine (!_). apply tensor_comp_mor. } refine (!(tensor_comp_mor _ _ _ _) @ _). rewrite id_right, id_left. etrans. { apply maponpaths. apply mon_lassociator_rassociator. } refine (_ @ tensor_id_id _ _). apply maponpaths_2. apply mon_rassociator_lassociator. - apply idpath. } rewrite id_right. etrans. { do 6 apply maponpaths_2. etrans. { apply pathsinv0, tensor_comp_id_r. } apply maponpaths_2. etrans. { apply pathsinv0, tensor_comp_id_l. } apply maponpaths. apply sym_mon_braiding_inv. } do 2 rewrite tensor_id_id. rewrite id_left. unfold middle. refine (!_). etrans. { apply maponpaths_2. apply tensor_split. } rewrite !assoc'. apply maponpaths. refine (!_). refine (!(id_left _) @ _). rewrite <- mon_lassociator_rassociator. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite mon_rassociator_rassociator. rewrite !assoc'. do 2 apply maponpaths. rewrite !assoc. rewrite <- !tensor_comp_id_r. rewrite mon_rassociator_lassociator. rewrite id_left. rewrite !tensor_comp_id_r. apply idpath. } etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite <- tensor_rassociator. apply idpath. } rewrite !assoc'. etrans. { do 3 apply maponpaths. refine (!(id_left _) @ _). rewrite <- tensor_id_id. rewrite <- mon_lassociator_rassociator. rewrite tensor_comp_id_l. rewrite !assoc'. apply maponpaths. rewrite !assoc. apply maponpaths_2. refine (!_). apply mon_rassociator_rassociator. } rewrite !assoc'. rewrite mon_rassociator_lassociator. rewrite id_right. refine (_ @ id_right _). rewrite <- mon_lassociator_rassociator. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. refine (!_). etrans. { do 2 apply maponpaths. rewrite <- tensor_id_id. apply tensor_lassociator. } etrans. { apply maponpaths. rewrite !assoc. rewrite mon_lassociator_lassociator. apply idpath. } rewrite !assoc. rewrite <- tensor_comp_id_r. rewrite mon_rassociator_lassociator. rewrite tensor_id_id. rewrite id_left. rewrite !assoc'. apply maponpaths. rewrite <- !tensor_comp_id_l. apply maponpaths. refine (!(id_left _) @ _). rewrite <- mon_rassociator_lassociator. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite mon_lassociator_lassociator. rewrite !assoc'. apply maponpaths. rewrite <- tensor_comp_id_l. rewrite mon_lassociator_rassociator. rewrite tensor_id_id. apply id_right. - rewrite tensor_comp_id_l. rewrite tensor_comp_id_r. rewrite assoc'. match goal with | [|- ?s · _ = _ ] => set (symzy := s) end. etrans. { do 5 apply maponpaths. etrans. { do 2 apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. apply pathsinv0, tensor_rassociator. } rewrite !tensor_comp_id_l. rewrite !assoc'. apply maponpaths. apply maponpaths_2. refine (!(id_right _) @ _). etrans. { apply maponpaths. apply pathsinv0, mon_rassociator_lassociator. } rewrite assoc. apply maponpaths_2. etrans. { apply tensor_rassociator. } rewrite tensor_id_id. apply maponpaths. assert (auxH := tensor_swap (mon_lassociator x1 y2 x2) (sym_mon_braiding V y1 z1 #⊗ identity z2) ). do 3 rewrite <- tensor_mor_right in auxH. transparent assert (auxiso : (z_iso ((x1 ⊗ y2 ⊗ x2) ⊗_{ V} (z1 ⊗ y1 ⊗ z2)) ((x1 ⊗ (y2 ⊗ x2)) ⊗_{ V} (z1 ⊗ y1 ⊗ z2)))). { apply (functor_on_z_iso (rightwhiskering_functor V _)). exact (z_iso_from_associator_iso V _ _ _). } apply (z_iso_inv_on_left _ _ _ _ auxiso) in auxH. cbn in auxH. clear auxiso. rewrite tensor_mor_right in auxH. exact auxH. } change ((pr12 V) y1 z1) with (sym_mon_braiding V y1 z1). rewrite !assoc. match goal with | [|- _ · ?s · _ · _ · _ · _ · _ = _ ] => set (symyz := s) end. etrans. { do 6 apply maponpaths_2. rewrite !assoc'. apply maponpaths. intermediate_path (identity (x1 ⊗ (y2 ⊗ x2) ⊗ (y1 ⊗ z1 ⊗ z2))). - etrans. { do 3 apply maponpaths. rewrite !assoc. etrans. { do 2 apply maponpaths_2. etrans. { apply maponpaths. apply maponpaths_2. exact (!(tensor_id_id _ _)). } refine (!_). apply tensor_rassociator. } rewrite !assoc'. apply maponpaths. rewrite !assoc. etrans. { apply maponpaths_2. apply mon_rassociator_rassociator. } rewrite !assoc'. rewrite tensor_mor_right. rewrite <- tensor_comp_id_r. rewrite mon_rassociator_lassociator. rewrite tensor_id_id. rewrite id_right. apply idpath. } refine (_ @ mon_lassociator_rassociator _ _ _). rewrite !assoc. apply maponpaths_2. etrans. { do 3 apply maponpaths_2. rewrite <- tensor_id_id. rewrite tensor_lassociator. apply idpath. } rewrite !assoc'. refine (_ @ id_right _). apply maponpaths. rewrite <- !tensor_comp_id_l. refine (_ @ tensor_id_id _ _). apply maponpaths. refine (_ @ mon_lassociator_rassociator _ _ _). rewrite !assoc. apply maponpaths_2. rewrite <- tensor_id_id. rewrite tensor_lassociator. rewrite !assoc'. refine (_ @ id_right _). apply maponpaths. rewrite <- !tensor_id_id. rewrite <- !tensor_comp_id_l. do 2 apply maponpaths. rewrite !tensor_id_id. apply mon_lassociator_rassociator. - apply idpath. } rewrite id_right. etrans. { do 5 apply maponpaths_2. etrans. { apply pathsinv0, tensor_comp_id_l. } apply maponpaths. etrans. { apply pathsinv0, tensor_comp_id_r. } apply maponpaths_2. apply sym_mon_braiding_inv. } do 2 rewrite tensor_id_id. rewrite id_left. unfold middle. refine (!_). etrans. { apply maponpaths_2. rewrite tensor_split'. apply idpath. } rewrite tensor_mor_right. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_id_id. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite <- !tensor_comp_id_l. apply maponpaths. refine (_ @ id_right _). rewrite <- mon_lassociator_rassociator. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. refine (!_). etrans. { do 2 apply maponpaths. apply mon_lassociator_lassociator. } rewrite !assoc. refine (_ @ id_left _). apply maponpaths_2. refine (_ @ mon_rassociator_lassociator _ _ _). apply maponpaths_2. refine (_ @ id_right _). rewrite !assoc'. apply maponpaths. rewrite <- tensor_id_id. rewrite <- tensor_comp_id_r. rewrite mon_rassociator_lassociator. apply idpath. 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.Isos. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import BifunctorNotations. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import MonoidalNotations.