Definition monoid_to_category (Mon : monoid) : contr_cat. Proof. use tpair. - use makecategory. + exact unit. + intros; exact Mon. + intros; apply setproperty. + intros; exact (unel Mon). + intros; exact (f * g). + intros; apply lunax. + intros; apply runax. + intros; cbn; symmetry; apply assocax. + intros; cbn; apply assocax. - apply iscontrunit. 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.