Notation [00EQ]

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 .