{M N : Monoid} : MonoidIsomorphism M N -> MonoidIsomorphism N M := fun f => Build_MonoidIsomorphism _ _ (Build_MonoidHomomorphism f^-1 _) _. Global Instance reflexive_monoidisomorphism : Reflexive MonoidIsomorphism := fun M => mnd_iso_id. Global Instance symmetric_monoidisomorphism : Symmetric MonoidIsomorphism := fun M N => . Global Instance transitive_monoidisomorphism : Transitive MonoidIsomorphism := fun M N P f g => mnd_iso_compose g f. Global Instance isgraph_monoid : IsGraph Monoid := Build_IsGraph Monoid MonoidHomomorphism. Global Instance is01cat_monoid : Is01Cat Monoid := Build_Is01Cat Monoid _ (@mnd_homo_id) (@mnd_homo_compose). Local Notation mnd_homo_map' M N := (@mnd_homo_map M N : _ -> (monoid_type M $-> _)). Global Instance is2graph_monoid : Is2Graph Monoid := fun M N => isgraph_induced (mnd_homo_map' M N). Global Instance isgraph_monoidhomomorphism {M N : Monoid} : IsGraph (M $-> N) := isgraph_induced (mnd_homo_map' M N). Global Instance is01cat_monoidhomomorphism {M N : Monoid} : Is01Cat (M $-> N) := is01cat_induced (mnd_homo_map' M N). Global Instance is0gpd_monoidhomomorphism {M N : Monoid} : Is0Gpd (M $-> N) := is0gpd_induced (mnd_homo_map' M N). Global Instance is0functor_postcomp_monoidhomomorphism {M N P : Monoid} (h : N $-> P) : Is0Functor (@cat_postcomp Monoid _ _ M N P h). Proof. apply Build_Is0Functor. intros ? ? p a; exact (ap h (p a)). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Equivalences Basics.Trunc. Require Import Types.Sigma Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Induced WildCat.Equiv WildCat.Universe Require Import (notations) Classes.interfaces.canonical_names.