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