Definition monoid_presheaf_action_equivalence : adj_equivalence_of_cats monoid_presheaf_to_action. Proof. use rad_equivalence_of_cats. - apply is_univalent_functor_category. apply is_univalent_HSET. - intros P P'. use isweq_iso. + intro f. use make_nat_trans. * intros t. induction t. exact (f : monoid_action_morphism _ _). * abstract ( intros t t'; induction t, t'; intro m; apply funextfun; intro x; apply (mor_action f) ). + abstract ( intro f; apply nat_trans_eq_alt; intro t; now induction t ). + abstract ( intro f; now apply monoid_action_morphism_eq ). - intro X. apply hinhpr. exists (monoid_action_to_presheaf_ob X). use make_z_iso. + apply (identity X). + apply (identity X). + abstract ( split; now apply monoid_action_morphism_eq ). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.Categories.Monoid. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.AlgebraicTheories.FundamentalTheorem.CommonUtilities.MonoidActions.