# nLab magmoidal groupoid

Contents

### Context

#### Algebra

higher algebra

universal algebra

categorification

category theory

# Contents

## Idea

In category theory, the notion of a magmoidal groupoid is the groupoidal categorification of the notion of magma, hence a magmoidal groupoid is simply a groupoid equipped with a “binary operation” on it. Similarly, under the relation between category theory and type theory, in homotopy type theory a magmoidal groupoid is a 1-truncated type equipped with a binary operation.

## Definitions

### In type theory

In intensional type theory with function extensionality, a groupoid is a 1-truncated type and a binary operation on a groupoid $G$ is a function $(-)\otimes (-) \colon G \times G \to G$ from the product groupoid $G \times G$ to $G$. A magmoidal groupoid $(G,\otimes)$ is a groupoid equipped with a binary operation on it.

### In category theory

In category theory, a groupoid is a dagger category where every morphism is unitary, and a binary operation on a groupoid $G$ is a dagger functor $(-)\otimes (-) \colon G \times G \to G$ from the product groupoid? $G \times G$ to $G$. A magmoidal groupoid $(G,\otimes)$ is a groupoid equipped with a binary operation on it.