Clearly we cannot define E on the whole universe, but only on a subuniverse.For example, we could define it on the subuniverse of types with finitely generated homology groups. For the Euler characteristic we will also need that the betti numbers are eventually 0. Other than that, I agree that these properties should hold in HoTT.