Definition contr_category_to_monoid (C : category) (is : iscontr (ob C)) : monoid. Proof. pose (center := iscontrpr1 is). use make_monoid. - use make_setwithbinop. + use make_hSet. * use (center --> center). * apply homset_property. + exact (@compose _ center center center). - use make_ismonoidop. + unfold isassoc; symmetry; apply assoc. + use make_isunital. * apply identity. * use make_isunit; [ unfold islunit; apply id_left | unfold isrunit; apply id_right ]. 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.