proposition: Lemma precategory_monoid_has_homsets: has_homsets precategory_monoid.
proof: Proof. red. intros X Y. red. intros f g. apply (isofhlevelweqf 1 (monoid_mor_eq(f := f)(g := g))). apply homset_property. Qed.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored