The addition from my second email didn't make sense, sorry. The first email 
with the easy argument should be correct.
Nicolai 

On Friday, September 7, 2018 at 7:30:23 AM UTC+1, Nicolai Kraus wrote:
>
> 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
>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.