We currently have enough machinary to (kind of) define Betti numbers (for homology see
Floris van Doorn's thesis). I am confident that soon we can start compting Betti numbers of some types. This would allow us to define the euler characterstic E : U --> N of a type. If classical algebraic topology tells us anything this will satisfy a lot of neat identities.
In fact consider U as a semiring with + and * as the operations. E is a semiring homomorphism to N (the initial semiring (is this relavent?)). In other words we should have
E(X + Y) = E(X) + E(Y)
E(X * Y) = E(X) E(Y)
and even maybe, subject to some conditions, a given type family P : X --> U would satisfy E( (x : X) * P(x) ) = E(X) * E(P(x_0))
This would be a cool invariant to have. Unfortunately as it stands, homology is a bit unwieldy. Perhaps rationalising spaces would help?
Any thoughts or suggestions?