Is there any progress on proving the Hurewicz theorem in HoTT?
I wonder if we can adapt the following argument:
Define H_n(X; Z) as [S^{n+t}, X /\ K(X, t)] for some large t and pointed space X. The Hurewicz map is induced by a generator g : S^t->K(Z, t) of H_n(S^n). Given by postcomposition with (id_X /\ g).
H : [S^{n+t}, X /\ S^t] ---> [S^{n+k}, X /\ K(Z, t)]
Now since X is (n-1)-connected and it can be shown that g is n-connected (an (n+1)-equivalence in the answer), then it follows that (id_X /\ g)_* is an isomorphism.
The only trouble I see with this argument working is the definition of homology. Instead of having a large enough t floating around we would have to use a colimit and that might get tricky. Showing that g is n-connected is possible I think using some lemmas about modalities I can't name of the top of my head.
Do you think this argument will work? Let me know what you all think.
Thanks,
Ali Caglayan