Thierry caught a mistake in my answer, so both my counterexamples actually 
don't work at least for the strong requirement that Z is factor.

The problem is, that the cohomology classes/maps P->Z I use are not 
different over Q.

Am Dienstag, 27. November 2018 17:22:30 UTC-5 schrieb Michael Shulman:
>
> Suppose I have an (unpointed) type X such that (unreduced) H_n(X) or 
> H^n(X) is nonzero for some n.  In the application I have in mind, this 
> group is nonzero in a very strong sense, e.g. it has the integers as a 
> direct summand.  Can I conclude (without using excluded middle) that 
> ||X||? 
>

-- 
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.