Homotopy Type Theory groupoid enriched in monoids > history (Rev #1)

Contents

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