Is there any progress on proving the Hurewicz theorem=
in HoTT?

I stumbled across this mathoverflow ques=
tion: https://mathoverflow.net/questions/2831=
99/an-abstract-nonsense-proof-of-the-hurewicz-theorem

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 poi=
nted 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 us=
ing some lemmas about modalities I can't name of the top of my head.

=

-- Do you think this argument will work? Let me know wh=
at you all think.

Thanks,

Ali Caglayan

You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.

To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.

To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/f50d39d3-0017-4820-9c76-877760449e78%40googleg= roups.com.

------=_Part_7804_411767636.1564233525519-- ------=_Part_7803_1449496504.1564233525519--