Lemma skewMonoid_identity_laws (T : skewMonoid_data ) : skewMonoid_Mor_laws (identity T). Proof. split; simpl. - rewrite id_right. etrans;[apply pathsinv0, id_left|]. apply cancel_postcomposition. apply pathsinv0. apply (functor_id tensor). - apply id_right. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.SkewMonoidal.SkewMonoidalCategories.