proposition: Lemma monoid_weq_contr_category : monoid ≃ contr_cat.
proof: 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.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.PartA UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.catiso UniMath.CategoryTheory.Additive UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.Categories.HSET.Core