nLab H-groupoid

Binary operations

Context

Algebra

higher algebra

universal algebra

categorification

category theory

Binary operations

Definitions

In type theory

In intensional type theory with function extensionality, a groupoid is a 1-truncated type and a H-spatial groupoid, $A_2$-spatial groupoid, unital magmoidal groupoid, or magmoidal groupoid with unit is a groupoid that is also an H-space/$A_2$-space.

In category theory

In category theory, a unital magmoidal groupoid or magmoidal groupoid with unit is a magmoidal groupoid $(G, \otimes)$ with a unit $I$ and natural unitary isomorphisms $\lambda_A \colon A\otimes I \simeq^\dagger A$ and $\rho_A \colon I\otimes A \simeq^\dagger A$.