Can it be done with excluded middle?

On Tuesday, 27 November 2018 22:22:30 UTC, Michael Shulman wrote:
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.