proposition: Lemma monoid_fun_weq_functor {Mon1 Mon2 : monoid} : (monoidfun Mon1 Mon2) ≃ functor (monoid_weq_contr_category Mon1) (monoid_weq_contr_category Mon2).
proof: 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.
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