`Index.card` has an extra universe parameter

[JamesGallicchio]

As in title.

set_option pp.universes true
#check IndexType.card (Prod (Fin 2) (Fin 2))
-- IndexType.card.{0, u_1} (Prod.{0, 0} (Fin 2) (Fin 2))

Probably we should not require Fold in the definition of IndexType, instead just expecting the universe to be Fold at any functions that need it.