Definition. Groupoid Cardinality of 1-types [00ER]

Let be a 1-type such that is finite, and for all is finite. Define the groupoid cardinality of as the rational number

where denotes a finite sum over rational numbers indexed by the finite set .