For a type write for .

For a -type and write for the set .

Given a 1-type , denote by the set cardinality of the set of automorphisms. The universal property of the set truncation gives a unique map from to , that is compatible with the Automorphism-Cardinality. By abuse of notation we also denote this map by .

We assume some construction of type of rational numbers. We assume that this type is a set with decidable equality, equipped with the usual addition and multiplication making it a field. We denote the field of rational numbers with . For a sketched construction see the HoTT book, section 11., section 11.1.

TODO: Make very clear what for what properties we need witnesses and find a construction we can borrow.

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 .

TODO

TODO

TODO