Lemma precompose_inner_swap_with_lunitors_and_runitor (x y : V) : inner_swap x (monoidal_unit V) y (monoidal_unit V) · (x ⊗ y) ⊗^{V}_{l} mon_lunitor (monoidal_unit V) · mon_runitor (x ⊗ y) = (mon_runitor x #⊗ mon_runitor y). Proof. unfold inner_swap. rewrite ! (bifunctor_leftcomp V). etrans. { apply maponpaths_2. rewrite ! assoc'. do 2 apply maponpaths. refine (_ @ idpath (x ⊗^{V}_{l} (mon_lunitor y ⊗^{V}_{r} monoidal_unit V) · mon_rassociator _ _ _)). apply pathsinv0. use (z_iso_inv_to_left _ _ _ (_ ,, _)). { use is_z_iso_leftwhiskering_z_iso. use (is_z_iso_rightwhiskering_z_iso V). apply (_ ,, monoidal_braiding_inverses V _ _). } cbn. rewrite ! assoc. rewrite <- (bifunctor_leftcomp V). etrans. { apply maponpaths_2. apply maponpaths. refine (! bifunctor_rightcomp V _ _ _ _ _ _ @ _). apply maponpaths. apply sym_mon_braiding_lunitor. } etrans. { apply maponpaths_2. apply maponpaths. refine (_ @ mon_triangle _ _). apply pathsinv0. apply (when_bifunctor_becomes_rightwhiskering V). } cbn. rewrite (bifunctor_leftcomp V). rewrite ! assoc'. apply maponpaths. unfold monoidal_cat_tensor_mor. cbn. rewrite (when_bifunctor_becomes_leftwhiskering V). apply (monoidal_associatorinvnatleft V). } rewrite ! assoc'. etrans. { do 3 apply maponpaths. apply mon_runitor_triangle. } unfold monoidal_cat_tensor_mor. cbn. unfold functoronmorphisms1. unfold monoidal_cat_tensor_pt. cbn. rewrite ! assoc. apply maponpaths_2. rewrite (bifunctor_rightid V). rewrite id_right. rewrite assoc'. rewrite <- (bifunctor_leftcomp V). etrans. 2: { refine (! mon_triangle _ _ @ _). apply (when_bifunctor_becomes_rightwhiskering V). } apply maponpaths. rewrite <- (when_bifunctor_becomes_leftwhiskering V). apply maponpaths. use (z_iso_inv_on_right _ _ _ (mon_lassociator _ _ _ ,, _ ,, _)). { apply monoidal_associatorisolaw. } cbn. rewrite <- (when_bifunctor_becomes_rightwhiskering V). apply (! mon_lunitor_triangle _ _). 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.