Lemma monoid_weq_contr_category : monoid ≃ contr_cat. Proof. use weq_iso. - exact monoid_to_category. - exact (uncurry contr_category_to_monoid). - intros Mon; apply monoid_univalence. use tpair. + apply idweq. + use make_dirprod. * intros ? ?; apply idpath. * apply idpath. - intros contrcat. use contr_cat_eq. + use make_functor. * apply contr_cat_functor_data. apply idfun. * use make_dirprod; cbn. { unfold functor_idax. intros a; cbn in *. abstract (induction a; reflexivity). } { unfold functor_compax. intros a b c. abstract (induction a, b, c; reflexivity). } + unfold fully_faithful. intros a b. abstract (induction a, b; exact (idisweq _)). 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.