Definition monoid_free_functor : functor HSET monoid_precategory. Proof. use make_functor. - use make_functor_data. + intros s; exact (free_monoid s). + intros ? ? f; exact (free_monoidfun f). - split. + intro. abstract (apply monoidfun_paths, funextfun; intro; apply map_idfun). + intros ? ? ? ? ?. abstract (apply monoidfun_paths, funextfun, (free_monoidfun_comp_homot f g)). 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.