Re: [HoTT] Looking for a reference that HITs are a strict extension of HoTT

[Nicolai Kraus <nicolai.kraus@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1957 bytes --]

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

> On 07/09/18 04:56, Jasper Hugunin wrote:
>> Hello all,
>>
>> Many ways of doing HoTT (Coq + Univalence Axiom, Cubical Type Theory) 
>> make sense without including support for defining Higher Inductive 
>> Types. The possibility of defining small, closed types which are not 
>> hsets (like the circle) or have infinite h-level (like the 2-sphere, 
>> conjectured?) makes constructing HITs from other types seem 
>> difficult, since all the type formers except universes preserve h-level.
>>
>> Does anyone know a proof that it is impossible to construct some HITs 
>> from basic type formers (say 0, 1, 2, Sigma, Pi, W, and a hierarchy 
>> of univalent universes U_n), up to equivalence?
>>
>> - Jasper Hugunin
>>
>> -- 
>> 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 
>> <mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>.
>> For more options, visit https://groups.google.com/d/optout.
>

-- 
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.

[-- Attachment #2: Type: text/html, Size: 3503 bytes --]