Lemma monoid_fun_weq_functor {Mon1 Mon2 : monoid} : (monoidfun Mon1 Mon2) ≃ functor (monoid_weq_contr_category Mon1) (monoid_weq_contr_category Mon2). Proof. use weq_iso. - exact monoidfun_to_functor. - exact functor_to_monoidfun. - intros mfun. apply monoidfun_paths. reflexivity. - intros funct. apply functor_eq; [apply homset_property|]. use functor_data_eq. + intro. exact (!(pr2 iscontrunit _)). + intros c1 c2 ?. abstract (induction c1, c2; unfold Univalence.double_transport; cbn; do 2 (rewrite (transport_f_f _ (isProofIrrelevantUnit _ _) (! (isProofIrrelevantUnit _ _)) _); rewrite pathsinv0r; cbn; unfold idfun); reflexivity). 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.