(M N : Monoid) := { mnd_iso_homo :> MonoidHomomorphism M N; isequiv_mnd_iso :: IsEquiv mnd_iso_homo; }.
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.