Definition monoidfun_to_functor {Mon1 Mon2 : monoid} (monfun : monoidfun Mon1 Mon2) : functor (monoid_weq_contr_category Mon1) (monoid_weq_contr_category Mon2). Proof. use make_functor. - apply contr_cat_functor_data. exact monfun. - use make_dirprod. + intros a. abstract (induction a; apply monoidfununel). + intros a b c ? ?. abstract (induction a, b, c; apply monoidfunmul). Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.Categories.HSET.Core.