Recently, there was a post about the Euler characteristic of a type. In my case, I am interested in the Hodge structure of the Hilbert scheme of n points on a 2-dimensional torus. Does such a topological construction make sense in HoTT for an arbitrary type, under some general hypothesis?
Kind Regards,
Jose M