Re: [HoTT] Semantics of QIITs ?

[Bas Spitters <b.a.w.spitters@gmail.com>]

As you say, Mike and Peter note that:
"the idea is that higher inductive types can be used to construct free
algebras for infinitary algebraic theories. However, Blass showed
(modulo a large
cardinal assumption) that these cannot be constructed in ZF [Bla83]."
In fact, they construct an uncountable regular cardinal explicitly (Thm 9.1).
https://arxiv.org/abs/1705.07088
So, QITs do add extra expresivity.


My question is about "small" QIITs (Cauchy reals, ...) in homotopical
models, so the setoid model does not really count.
However, has it been proved even in that case that such QIITs exist?

On Mon, May 20, 2019 at 6:17 PM Thorsten Altenkirch
<Thorsten.Altenkirch@nottingham.ac.uk> wrote:
>
> Do we know wether the existence of QI(I)Ts isn't a new constructive principle?
>
> Mike and Peter show that there are QITs which aren't constructible from quotients. However, we may still be able to justify a type theory with QITs without using them. E.g. in the Setoid model we can construct many QITs including the Reals (I think) but this is maybe because choice is provable for the setoids which are obtained from sets (like Nat). But what about a QIT which uses a setoid for which we don't have choice?
>
> Thorsten
>
>
> On 16/05/2019, 19:50, "Bas Spitters" <b.a.w.spitters@gmail.com> wrote:
>
>     Thanks for confirming that this is still open in homotopical models.
>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> --
> 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/68D3FF39-6345-47B0-B905-72BDD282583A%40exmail.nottingham.ac.uk.
> 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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRJ5QU2GTqctjGSJax0CXkBWWq7GEYcf0EEox3izZTDeQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.