nLab magmoidal groupoid

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.

See also

• magma
• groupoid
• H-spatial groupoid
• magmoidal category