Definition monoid_forgetful_functor : functor monoid_precategory HSET. Proof. use make_functor. - use make_functor_data. + intro; exact (pr1setwithbinop (pr1monoid ltac:(assumption))). + intros ? ? f; exact (pr1monoidfun _ _ f). - split. + intro; reflexivity. + intros ? ? ? ? ?; reflexivity. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Free_Monoids_and_Groups. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Adjunctions.Core.