Re: [HoTT] Semantics of QIITs ?

[Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk>]

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.