Re: [HoTT] Semantics of QIITs ?

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

Hi Jon,

Thank you for this explanation. Indeed, I think the question of how to interpret QITs without UIP is interesting and open. 

I do think the setoid model is useful in this context. It can be defined without using UIP by using propositional relations. Within this model you have limited instances of choice, namely for types that can be obtained by the embedding. Hence I think that QITs that just require countable choice like the Reals should not be a problem. However, this does not give you an explanation for infinitary QITs indexed over a QIT but I don't actually know a natural example of such a thing.

Thorsten

On 21/05/2019, 00:26, "homotopytypetheory@googlegroups.com on behalf of Jon Sterling" <homotopytypetheory@googlegroups.com on behalf of jon@jonmsterling.com> wrote:

    Dear Thorsten,
    
    As Andras noted in his message to this thread, it is very much an open question whether QIITs can be modeled without using UIP (this is part of what people are trying to distinguish from, when they are asking about "homotopical" models);  therefore, "interpreting them in cubical sets using the general construction of HITs" is definitely not a slam-dunk, and novel + worthwhile research will be needed to determine if it works.
    
    Echoing Andras, I recall that a new encoding due to Jasper Hugunin enable us to interpret IITs without using UIP, and it is an open question to determine whether Jasper's ideas can be extended to QIITs. I hope they can, and someone should find out :)
    
    Best,
    Jon
    
    
    On Mon, May 20, 2019, at 6:17 PM, Thorsten Altenkirch wrote:
    > What exactly do you mean by “a model”? I’d think we can interpret them 
    > in cubical sets using the general construction of HITs. They don’t seem 
    > to cause problems in cubical Agda as far as I can see.
    > 
    > Sent from my iPhone
    > 
    > > On 20 May 2019, at 22:04, Bas Spitters <b.a.w.spitters@gmail.com> wrote:
    > > 
    > > Do we even have a model that would capture all the QIIT constructions
    > > in the HoTT book?
    > > 
    > > I recall an argument where one constructs the Cauchy numbers as a QIIT
    > > *within* the Dedekind numbers (assuming impredicativity) and then show
    > > that this indeed has the right initiality property. However, I don't
    > > recall whether anyone ever worked out the details of this, or how
    > > general this method is.
    > > 
    > >> On Mon, May 20, 2019 at 9:59 PM Jon Sterling <jon@jonmsterling.com> wrote:
    > >> 
    > >> Hi Thorsten,
    > >> 
    > >> I think that in the way I interpreted Bas's question, setoids probably don't count --- by that token, even sets would also be "homotopical" because sets are a special case of setoids which are a special case of groupoids which are a special case of infinity groupoids, but what people are wondering is probably more along the lines of whether there is a model of type theory in which the universes are both univalent and closed under general QIITs. And as Bas notes, non-finitary QIITs are not just a special case of something well-known like generalized algebraic theories or something like that, so there are some really deep questions involved.
    > >> 
    > >> This is not a bad thing: it means there are some very interesting questions left to figure out, maybe suitable for an ambitious phd student :)
    > >> 
    > >> Best,
    > >> Jon
    > >> 
    > >> 
    > >> 
    > >> 
    > >>> On Mon, May 20, 2019, at 2:36 PM, Thorsten Altenkirch wrote:
    > >>> The setoid model is just a restriction of the groupoid model where all
    > >>> the Homs are propositional - does this not count as homotopical?
    > >>> 
    > >>> 
    > >>> 
    > >>> Sent from my iPhone
    > >>> 
    > >>>> On 20 May 2019, at 18:55, Bas Spitters <b.a.w.spitters@gmail.com> wrote:
    > >>>> 
    > >>>> 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.
    > >>> 
    > >>> 
    > >>> 
    > >>> 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/FBCD91A3-4A6F-456E-93FA-E36EFB56D607%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/b704d949-bf4b-4898-bee1-594cc7343de5%40www.fastmail.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.
    > > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuSYrG-u-i7jTvRHr6usa-PhMWs0SvD2HuMw0__z5DMPwg%40mail.gmail.com.
    > > For more options, visit https://groups.google.com/d/optout.
    > 
    > 
    > 
    > 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/4CAE313E-7B00-41D3-A13A-3AAC0A496AB0%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/96fea5d2-535c-43fc-9832-48ce96e916ca%40www.fastmail.com.
    For more options, visit https://groups.google.com/d/optout.
    




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/29D54132-775E-43EE-8439-544FF3EA6C4F%40nottingham.ac.uk.
For more options, visit https://groups.google.com/d/optout.