proposition: Lemma precompose_inner_swap_with_lunitors_on_right (x y : V) : inner_swap (monoidal_unit V) x (monoidal_unit V) y · mon_lunitor (monoidal_unit V) ⊗^{V}_{r} (x ⊗ y) · mon_lunitor (x ⊗ y) = (mon_lunitor x #⊗ mon_lunitor y).
proof: Proof. unfold inner_swap. rewrite ! (bifunctor_leftcomp V). etrans. { apply maponpaths_2. rewrite ! assoc'. do 2 apply maponpaths. refine (_ @ idpath (monoidal_unit V ⊗^{V}_{l} (mon_runitor x ⊗^{V}_{r} y))). 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 <- (bifunctor_leftcomp V). etrans. { apply maponpaths. refine (! bifunctor_rightcomp V _ _ _ _ _ _ @ _). apply maponpaths. apply sym_mon_braiding_runitor. } apply whiskering_on_both_sides_with_lunitor_left_unit. } rewrite <- (bifunctor_leftcomp V). etrans. { apply maponpaths_2. do 2 apply maponpaths. etrans. { apply maponpaths. refine (_ @ mon_triangle x y). apply pathsinv0, (when_bifunctor_becomes_rightwhiskering V). } rewrite assoc. apply maponpaths_2. apply monoidal_associatorisolaw. } rewrite id_left. unfold monoidal_cat_tensor_mor. cbn. etrans. { rewrite assoc'. apply maponpaths. refine (_ @ tensor_lunitor (identity x #⊗ mon_lunitor y)). now rewrite <- (when_bifunctor_becomes_leftwhiskering V). } rewrite assoc. etrans. { apply maponpaths_2. apply mon_lunitor_triangle. } apply pathsinv0, tensor_split'. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric