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