CatGloss
A
groupoid
is a category in which every morphism is an isomorphism.