Lemma I_mult_laws (V : skewmonoidal_category) (X : V) : α' I I X · identity (C := V) I #⊗ λ' X · λ' X = λ' I #⊗ identity X · λ' X. Proof. etrans. { etrans;[apply pathsinv0,assoc|]. apply cancel_precomposition. apply skewmonoidal_unitl_ax. } rewrite assoc. apply cancel_postcomposition. apply skewmonoidal_alpha_lambda_eq. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering.