Groupoid

In mathematics, especially in category theory and homotopy theory, a groupoid (less often Brandt groupoid or virtual group) generalises the notion of group in several equivalent ways. A groupoid can be seen as a:

• Group with a partial function replacing the binary operation;
• Category in which every morphism is invertible. A category of this sort can be viewed as augmented with a unary operation on the morphisms, called inverse by analogy with group theory. A groupoid where there is only one object is a usual group.

In the presence of dependent typing, a category in general can be viewed as a typed monoid, and similarly, a groupoid can be viewed as simply a typed group. The morphisms take one from one object to another, and form a dependent family of types, thus morphisms might be typed ⁠$g:A\rightarrow B$⁠, ⁠$h:B\rightarrow C$⁠, say. Composition is then a total function: ⁠$\circ$ :(B\rightarrow C)\rightarrow (A\rightarrow B)\rightarrow (A\rightarrow C) ⁠, so that ⁠$h\circ g:A\rightarrow C$⁠.

Special cases include:

• Setoids: sets that come with an equivalence relation,
• G-sets: sets equipped with an action of a group ⁠$G$⁠.

Groupoids are often used to reason about geometrical objects such as manifolds. Heinrich Brandt (1927) introduced groupoids implicitly via Brandt semigroups.