Lemma precategory_monoid_has_homsets: has_homsets precategory_monoid. Proof. red. intros X Y. red. intros f g. apply (isofhlevelweqf 1 (monoid_mor_eq(f := f)(g := g))). apply homset_property. 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.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored.