Small addition to my first remark:
On 07/09/18 07:14, Nicolai Kraus wrote:
Remarks: 1. If we knew that S^2 is not a k-type for any k, then this would work as well for the second step, but as you said, we don't know so far whether this can be shown in HoTT.
Since we don't need an internal argument, it should be possible to use S^2 together with Thierry's result in Christian's post
https://groups.google.com/forum/#!topic/ homotopytypetheory/imPb56IqxOI
But this is only for CCHM type theory.
Nicolai