Lemma precategory_skewMonoid_axioms : is_precategory precategory_skewMonoid_data. Proof. repeat split; simpl; intros. - apply (invmap (skewMonoid_Mor_equiv _ _ )). apply id_left. - apply (invmap (skewMonoid_Mor_equiv _ _ )). apply id_right. - apply (invmap (skewMonoid_Mor_equiv _ _ )). apply assoc. - apply (invmap (skewMonoid_Mor_equiv _ _ )). apply assoc'. 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.