This would be some subuniverse of "compact" spaces I assume. On Monday, 17 September 2018 23:37:03 UTC+1, Floris van Doorn wrote: > > 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. > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.