Proposition pairing_lassociator {a x y z : C} (f : a --> x) (g : a --> y) (h : a --> z) : ⟨⟨f,g⟩,h⟩ · mon_lassociator _ _ _ = ⟨f,⟨g,h⟩⟩. Proof. rewrite <- (id_left h). rewrite (pairing_eq f g). rewrite <- pairing_tensor. unfold pairing. rewrite copy_assoc. rewrite !assoc'. rewrite tensor_lassociator. etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite mon_rassociator_lassociator. apply id_left. } rewrite <- tensor_comp_mor. rewrite !id_left. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.SymmetricDiagonal. Import MonoidalNotations.