Milnor's countable join is contractible

The countable join universalGSpace G of a nonempty type G is weakly contractible (TauCeti.subsingleton_homotopyGroup_universalGSpace) and carries a CW structure, so it is contractible by Whitehead's theorem (TauCeti.instContractibleSpaceUniversalGSpace).

References

• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.

instance TauCeti.instContractibleSpaceUniversalGSpace (G : Type u) [Nonempty G] : ContractibleSpace (universalGSpace G)

Milnor's countable join is contractible: it is weakly contractible, and it has CW type through its CW structure whose cells are the simplices of the countable join, so Whitehead's theorem applies.