[[!redirects groupoids enriched in monoids]] ## Contents ## * table of contents {:toc} ## Definition A __groupoid enriched in monoids__ consists of * A [[type]] $A$ * A enricher-in-monoids $$\eta_\mathrm{Mon}: \prod_{(a:A)} \prod_{(b:A)} \mathrm{isMonoid}(a = b)$$ ## See also * [[groupoid]] * [[monoid]]