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