[HoTT] Re: Semantics of QIITs ?

[Andrew Swan <wakelin.swan@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1762 bytes --]

Regarding the Cauchy reals, I believe it is known that countable choice 
holds and set quotients exist in simplicial sets, but I think under these 
conditions the usual construction of the Cauchy reals as a quotient of 
sequences of rationals satisfies the constructors for the HIT Cauchy reals, 
and also the higher induction principle.

I think the HIT cumulative hierarchy can be constructed using W types and 
univalence, using the characterisation of it as a retract of the Aczel 
cumulative hierarchy by Hakon Gylterud in the paper 
at https://doi.org/10.1017/jsl.2017.84 . If so, similar arguments should 
work for ordinals and surreal numbers.

Are there any other examples in the HoTT book?

Best,
Andrew

On Thursday, 16 May 2019 16:57:36 UTC+2, Bas Spitters wrote:
>
> What is the status of the semantics of quotient inductive inductive types? 
> Looking at the literature there's some progress on reducing QIITs to 
> simpler constructions, but this does not seem to have led to a 
> convenient semantic result. 
> E.g. QIITs do not seem to be treated in the work by Lumdaine and Shulman. 
>
> https://ncatlab.org/nlab/show/inductive-inductive+type 
>
> Do we know that the prototypical QIITs from the book (e.g. Cauchy 
> reals) are supported in the usual models of HoTT? 
>
> Thanks, 
>
> Bas 
>

-- 
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/f580d237-12b5-4107-92c4-7738fd89e59f%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 2901 bytes --]