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/CAOoPQuQBwyvbY_f3qNZOgEB7nxQHGUigqXjNhbDmCvB3xnVaOw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

Hi Bas, Our POPL 2019 paper does address this I think, maybe not exactly in the way you expect. We define a theory of codes (based on earlier work by Ambrus and Andras) which is an intrinsic type theory such that a context is a representation of a quotient inductive-inductive type. The formation of Pi-types is restricted so that you can only form strictly positive types, it is indeed a special case of a directed type theory. Now the semantics are categories with an initial object and it turns out we can construct the semantics just from assuming the existence of the theory of codes. The category assigned to a context is the category of algebras and the initial object is the intended interpretation of the QIIT, equivalently we get the expected elimination principle. The theory of codes can "eat itself" it is an instance of a QIIT definable in itself. Hence this QIIT is in a certain sense universal. One would also like to interpret QIITs that are indexed by "external" types which are already defined and in particular include infinitary constructors. One can extend the theory but the semantics suffered from a coherence issue. However, I think Andras made some progress on this. My view is that this programme can be extended to HIITs by considering higher order versions of type theory and in particular the theory of codes. However, this is maybe an overkill, since one can normalize the substitutions (make them implicit) and address the coherence issues this way. I think that is basically what Andras has done. Here is a link to the pdf: https://akaposi.github.io/finitaryqiit.pdf Thorsten On 16/05/2019, 15:58, "homotopytypetheory@googlegroups.com on behalf of Bas Spitters" <homotopytypetheory@googlegroups.com on behalf of b.a.w.spitters@gmail.com> 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/CAOoPQuQBwyvbY_f3qNZOgEB7nxQHGUigqXjNhbDmCvB3xnVaOw%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/99645C4A-A893-459A-B027-5607E89A37EF%40nottingham.ac.uk. For more options, visit https://groups.google.com/d/optout.

Hi Thorsten, Yes, I saw your result (congratulations!) However, I may be overlooking something, but do we know that the theory of codes is available in any of the standard models of HoTT? That doesn't seem to be stated in your paper. Best regards, Bas On Thu, May 16, 2019 at 5:39 PM Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk> wrote: > > Hi Bas, > > Our POPL 2019 paper does address this I think, maybe not exactly in the way you expect. We define a theory of codes (based on earlier work by Ambrus and Andras) which is an intrinsic type theory such that a context is a representation of a quotient inductive-inductive type. The formation of Pi-types is restricted so that you can only form strictly positive types, it is indeed a special case of a directed type theory. Now the semantics are categories with an initial object and it turns out we can construct the semantics just from assuming the existence of the theory of codes. The category assigned to a context is the category of algebras and the initial object is the intended interpretation of the QIIT, equivalently we get the expected elimination principle. The theory of codes can "eat itself" it is an instance of a QIIT definable in itself. Hence this QIIT is in a certain sense universal. > > One would also like to interpret QIITs that are indexed by "external" types which are already defined and in particular include infinitary constructors. One can extend the theory but the semantics suffered from a coherence issue. However, I think Andras made some progress on this. > > My view is that this programme can be extended to HIITs by considering higher order versions of type theory and in particular the theory of codes. However, this is maybe an overkill, since one can normalize the substitutions (make them implicit) and address the coherence issues this way. I think that is basically what Andras has done. > > Here is a link to the pdf: > https://akaposi.github.io/finitaryqiit.pdf > > Thorsten > > On 16/05/2019, 15:58, "homotopytypetheory@googlegroups.com on behalf of Bas Spitters" <homotopytypetheory@googlegroups.com on behalf of b.a.w.spitters@gmail.com> 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/CAOoPQuQBwyvbY_f3qNZOgEB7nxQHGUigqXjNhbDmCvB3xnVaOw%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/CAOoPQuQT%2BcX7QbmKT%2BOsNgO%2BYGeDrqqOYXxcx714NWZo6ZO2bQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1: Type: text/plain, Size: 5521 bytes --] Hi, In "Constructing QIITs", we only considered signatures and their semantics in the setting of extensional TT. It is currently an open problem whether construction of QIITs (in the style of our paper) can be performed without UIP, and also whether the syntax of QIIT signatures itself is constructible in such setting. Jasper Hugunin's recent work on constructing some inductive-inductive types in cubical TT could relevant here. best regards András Bas Spitters <b.a.w.spitters@gmail.com> ezt írta (időpont: 2019. máj. 16., Cs, 17:50): > Hi Thorsten, > > Yes, I saw your result (congratulations!) However, I may be > overlooking something, but do we know that the theory of codes is > available in any of the standard models of HoTT? > That doesn't seem to be stated in your paper. > > Best regards, > > Bas > > > On Thu, May 16, 2019 at 5:39 PM Thorsten Altenkirch > <Thorsten.Altenkirch@nottingham.ac.uk> wrote: > > > > Hi Bas, > > > > Our POPL 2019 paper does address this I think, maybe not exactly in the > way you expect. We define a theory of codes (based on earlier work by > Ambrus and Andras) which is an intrinsic type theory such that a context is > a representation of a quotient inductive-inductive type. The formation of > Pi-types is restricted so that you can only form strictly positive types, > it is indeed a special case of a directed type theory. Now the semantics > are categories with an initial object and it turns out we can construct the > semantics just from assuming the existence of the theory of codes. The > category assigned to a context is the category of algebras and the initial > object is the intended interpretation of the QIIT, equivalently we get the > expected elimination principle. The theory of codes can "eat itself" it is > an instance of a QIIT definable in itself. Hence this QIIT is in a certain > sense universal. > > > > One would also like to interpret QIITs that are indexed by "external" > types which are already defined and in particular include infinitary > constructors. One can extend the theory but the semantics suffered from a > coherence issue. However, I think Andras made some progress on this. > > > > My view is that this programme can be extended to HIITs by considering > higher order versions of type theory and in particular the theory of codes. > However, this is maybe an overkill, since one can normalize the > substitutions (make them implicit) and address the coherence issues this > way. I think that is basically what Andras has done. > > > > Here is a link to the pdf: > > https://akaposi.github.io/finitaryqiit.pdf > > > > Thorsten > > > > On 16/05/2019, 15:58, "homotopytypetheory@googlegroups.com on behalf > of Bas Spitters" <homotopytypetheory@googlegroups.com on behalf of > b.a.w.spitters@gmail.com> 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/CAOoPQuQBwyvbY_f3qNZOgEB7nxQHGUigqXjNhbDmCvB3xnVaOw%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/CAOoPQuQT%2BcX7QbmKT%2BOsNgO%2BYGeDrqqOYXxcx714NWZo6ZO2bQ%40mail.gmail.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/CAA3CDBbsxaxrYsoabfNAP0DxLtqUATTOSW2PfX1EreKnOe2ozQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 7692 bytes --] <div dir="ltr">Hi,<div><br></div><div>In "Constructing QIITs", we only considered signatures and their semantics in the setting of extensional TT. It is currently an open problem whether construction of QIITs (in the style of our paper) can be performed without UIP, and also whether the syntax of QIIT signatures itself is constructible in such setting. Jasper Hugunin's recent work on constructing some inductive-inductive types in cubical TT could relevant here.</div><div><br></div><div>best regards</div><div>András</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Bas Spitters <<a href="mailto:b.a.w.spitters@gmail.com">b.a.w.spitters@gmail.com</a>> ezt írta (időpont: 2019. máj. 16., Cs, 17:50):<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Thorsten,<br> <br> Yes, I saw your result (congratulations!) However, I may be<br> overlooking something, but do we know that the theory of codes is<br> available in any of the standard models of HoTT?<br> That doesn't seem to be stated in your paper.<br> <br> Best regards,<br> <br> Bas<br> <br> <br> On Thu, May 16, 2019 at 5:39 PM Thorsten Altenkirch<br> <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br> ><br> > Hi Bas,<br> ><br> > Our POPL 2019 paper does address this I think, maybe not exactly in the way you expect. We define a theory of codes (based on earlier work by Ambrus and Andras) which is an intrinsic type theory such that a context is a representation of a quotient inductive-inductive type. The formation of Pi-types is restricted so that you can only form strictly positive types, it is indeed a special case of a directed type theory. Now the semantics are categories with an initial object and it turns out we can construct the semantics just from assuming the existence of the theory of codes. The category assigned to a context is the category of algebras and the initial object is the intended interpretation of the QIIT, equivalently we get the expected elimination principle. The theory of codes can "eat itself" it is an instance of a QIIT definable in itself. Hence this QIIT is in a certain sense universal.<br> ><br> > One would also like to interpret QIITs that are indexed by "external" types which are already defined and in particular include infinitary constructors. One can extend the theory but the semantics suffered from a coherence issue. However, I think Andras made some progress on this.<br> ><br> > My view is that this programme can be extended to HIITs by considering higher order versions of type theory and in particular the theory of codes. However, this is maybe an overkill, since one can normalize the substitutions (make them implicit) and address the coherence issues this way. I think that is basically what Andras has done.<br> ><br> > Here is a link to the pdf:<br> > <a href="https://akaposi.github.io/finitaryqiit.pdf" rel="noreferrer" target="_blank">https://akaposi.github.io/finitaryqiit.pdf</a><br> ><br> > Thorsten<br> ><br> > On 16/05/2019, 15:58, "<a href="mailto:homotopytypetheory@googlegroups.com" target="_blank">homotopytypetheory@googlegroups.com</a> on behalf of Bas Spitters" <<a href="mailto:homotopytypetheory@googlegroups.com" target="_blank">homotopytypetheory@googlegroups.com</a> on behalf of <a href="mailto:b.a.w.spitters@gmail.com" target="_blank">b.a.w.spitters@gmail.com</a>> wrote:<br> ><br> > What is the status of the semantics of quotient inductive inductive types?<br> > Looking at the literature there's some progress on reducing QIITs to<br> > simpler constructions, but this does not seem to have led to a<br> > convenient semantic result.<br> > E.g. QIITs do not seem to be treated in the work by Lumdaine and Shulman.<br> ><br> > <a href="https://ncatlab.org/nlab/show/inductive-inductive+type" rel="noreferrer" target="_blank">https://ncatlab.org/nlab/show/inductive-inductive+type</a><br> ><br> > Do we know that the prototypical QIITs from the book (e.g. Cauchy<br> > reals) are supported in the usual models of HoTT?<br> ><br> > Thanks,<br> ><br> > Bas<br> ><br> > --<br> > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> > To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com" target="_blank">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> > To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuQBwyvbY_f3qNZOgEB7nxQHGUigqXjNhbDmCvB3xnVaOw%40mail.gmail.com" rel="noreferrer" target="_blank">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuQBwyvbY_f3qNZOgEB7nxQHGUigqXjNhbDmCvB3xnVaOw%40mail.gmail.com</a>.<br> > For more options, visit <a href="https://groups.google.com/d/optout" rel="noreferrer" target="_blank">https://groups.google.com/d/optout</a>.<br> ><br> ><br> ><br> ><br> ><br> > This message and any attachment are intended solely for the addressee<br> > and may contain confidential information. If you have received this<br> > message in error, please contact the sender and delete the email and<br> > attachment.<br> ><br> > Any views or opinions expressed by the author of this email do not<br> > necessarily reflect the views of the University of Nottingham. Email<br> > communications with the University of Nottingham may be monitored<br> > where permitted by law.<br> ><br> ><br> ><br> ><br> <br> -- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com" target="_blank">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuQT%2BcX7QbmKT%2BOsNgO%2BYGeDrqqOYXxcx714NWZo6ZO2bQ%40mail.gmail.com" rel="noreferrer" target="_blank">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuQT%2BcX7QbmKT%2BOsNgO%2BYGeDrqqOYXxcx714NWZo6ZO2bQ%40mail.gmail.com</a>.<br> For more options, visit <a href="https://groups.google.com/d/optout" rel="noreferrer" target="_blank">https://groups.google.com/d/optout</a>.<br> </blockquote></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAA3CDBbsxaxrYsoabfNAP0DxLtqUATTOSW2PfX1EreKnOe2ozQ%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAA3CDBbsxaxrYsoabfNAP0DxLtqUATTOSW2PfX1EreKnOe2ozQ%40mail.gmail.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

Thanks for confirming that this is still open in homotopical models. -- 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/CAOoPQuRVR1A84pFE67GndjCHcUUV_vRCQ8UWdndai%2BzoiqqjZw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

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.

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.

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.

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.

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.

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.

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.

[-- Attachment #1.1: Type: text/plain, Size: 1383 bytes --] I'm not completely satisfied with Hugunin's technique, because it justifies only the "simple" elimination principle, rather than the general, "recursive-recursive" elimination principle implemented in Agda. As far as I can tell, realistic use cases for inductive-inductive families also need the recursive-recursive elimination principle, where the types of the maps out of later families depend on the maps out of earlier families. (I'm not sure how much of the other research on IIFs stops short of handling recursion-recursion, but I think it should be taken seriously.) On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote: > > 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 > -- 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/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 1898 bytes --] <div dir="ltr">I'm not completely satisfied with Hugunin's technique, because it justifies only the "simple" elimination principle, rather than the general, "recursive-recursive" elimination principle implemented in Agda. As far as I can tell, realistic use cases for inductive-inductive families also need the recursive-recursive elimination principle, where the types of the maps out of later families depend on the maps out of earlier families. (I'm not sure how much of the other research on IIFs stops short of handling recursion-recursion, but I think it should be taken seriously.)<br><br>On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">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 :) <br> <br>Best, <br>Jon<br></blockquote></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 3378 bytes --] Hello all, To confirm what others have said about my construction: As Andras and Jon noted, it remains open whether the construction can be extended to reduce higher inductive-inductive types to higher inductive types, but I am hopeful that it can, at least in a situation such as CTT where the eliminator computes on path constructors. As Matt noted, the general recursive-recursive eliminator is both essential (for proving initiality, for example) and missing. This is the same restriction as on the construction in extensional type theory (or using UIP) given by Nordvall Forsberg. The main obstacle I see to getting the general recursive-recursive eliminator is that the simple eliminator is not strict, but only computes up to a path. I think I see a way to turn a strict simple eliminator into a general eliminator, but this is still conjectural. To summarize my understanding of the original question, QIITs are an obvious subset of HIITs, and we know how to handle many HITs primitively in cubical type theory, but the extension to primitive HIITs in cubical type theory has not been done, nor does my construction immediately allow reducing HIITs to HITs (and even if extended lacks strictness and generality of the eliminator). Best regards, - Jasper Hugunin On Mon, May 20, 2019 at 5:28 PM Matt Oliveri <atmacen@gmail.com> wrote: > I'm not completely satisfied with Hugunin's technique, because it > justifies only the "simple" elimination principle, rather than the general, > "recursive-recursive" elimination principle implemented in Agda. As far as > I can tell, realistic use cases for inductive-inductive families also need > the recursive-recursive elimination principle, where the types of the maps > out of later families depend on the maps out of earlier families. (I'm not > sure how much of the other research on IIFs stops short of handling > recursion-recursion, but I think it should be taken seriously.) > > On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote: >> >> 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 >> > -- > 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/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com?utm_medium=email&utm_source=footer> > . > 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/CAGTS-a9F-8ph2U4MoPFaoTHam0SCTg3YZWAEJAjyLrrbBd71sw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 4514 bytes --] <div dir="ltr"><div dir="ltr">Hello all,<div><br></div><div>To confirm what others have said about my construction:</div><div>As Andras and Jon noted, it remains open whether the construction can be extended to reduce higher inductive-inductive types to higher inductive types, but I am hopeful that it can, at least in a situation such as CTT where the eliminator computes on path constructors.</div><div>As Matt noted, the general recursive-recursive eliminator is both essential (for proving initiality, for example) and missing. This is the same restriction as on the construction in extensional type theory (or using UIP) given by Nordvall Forsberg. The main obstacle I see to getting the general recursive-recursive eliminator is that the simple eliminator is not strict, but only computes up to a path. I think I see a way to turn a strict simple eliminator into a general eliminator, but this is still conjectural.</div><div><br></div><div>To summarize my understanding of the original question, QIITs are an obvious subset of HIITs, and we know how to handle many HITs primitively in cubical type theory, but the extension to primitive HIITs in cubical type theory has not been done, nor does my construction immediately allow reducing HIITs to HITs (and even if extended lacks strictness and generality of the eliminator).</div><div><div><br></div><div>Best regards,</div><div>- Jasper Hugunin</div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, May 20, 2019 at 5:28 PM Matt Oliveri <<a href="mailto:atmacen@gmail.com">atmacen@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">I'm not completely satisfied with Hugunin's technique, because it justifies only the "simple" elimination principle, rather than the general, "recursive-recursive" elimination principle implemented in Agda. As far as I can tell, realistic use cases for inductive-inductive families also need the recursive-recursive elimination principle, where the types of the maps out of later families depend on the maps out of earlier families. (I'm not sure how much of the other research on IIFs stops short of handling recursion-recursion, but I think it should be taken seriously.)<br><br>On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote:<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">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 :) <br> <br>Best, <br>Jon<br></blockquote></div> <p></p> -- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com" target="_blank">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com?utm_medium=email&utm_source=footer" target="_blank">https://groups.google.com/d/msgid/HomotopyTypeTheory/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com</a>.<br> For more options, visit <a href="https://groups.google.com/d/optout" target="_blank">https://groups.google.com/d/optout</a>.<br> </blockquote></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a9F-8ph2U4MoPFaoTHam0SCTg3YZWAEJAjyLrrbBd71sw%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a9F-8ph2U4MoPFaoTHam0SCTg3YZWAEJAjyLrrbBd71sw%40mail.gmail.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

[-- Attachment #1.1: Type: text/plain, Size: 3456 bytes --] This problem has been solved – see our TYPES 2018 abstract (attached). Basically the idea is to define a relation between “pre-terms” and the semantics and then show that this is contractible for “well-typed objects”, this way you avoid the mutual dependency. This was an idea by Andras Kovacs. In this year’s TYPES there are two abstracts that show how this can be used to give a universal reduction from Inductive-Inductive types to indexed inductive types and hence W-types. I have discussed this with Jesper when he was in Nottingham and I think our tentative conclusion was that this could be combined with his approach to provide a reduction for IITs. However, this needs to be checked. Thorsten From: <homotopytypetheory@googlegroups.com> on behalf of Matt Oliveri <atmacen@gmail.com> Date: Tuesday, 21 May 2019 at 01:28 To: Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: Re: [HoTT] Semantics of QIITs ? I'm not completely satisfied with Hugunin's technique, because it justifies only the "simple" elimination principle, rather than the general, "recursive-recursive" elimination principle implemented in Agda. As far as I can tell, realistic use cases for inductive-inductive families also need the recursive-recursive elimination principle, where the types of the maps out of later families depend on the maps out of earlier families. (I'm not sure how much of the other research on IIFs stops short of handling recursion-recursion, but I think it should be taken seriously.) On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote: 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 -- 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>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com?utm_medium=email&utm_source=footer>. 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/3DC3F379-F057-49AF-9232-CDC925E9646B%40nottingham.ac.uk. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 6591 bytes --] <html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"> <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8"> <meta name="Generator" content="Microsoft Word 15 (filtered medium)"> <style><!-- /* Font Definitions */ @font-face {font-family:"Cambria Math"; panose-1:2 4 5 3 5 4 6 3 2 4;} @font-face {font-family:Calibri; panose-1:2 15 5 2 2 2 4 3 2 4;} /* Style Definitions */ p.MsoNormal, li.MsoNormal, div.MsoNormal {margin:0cm; margin-bottom:.0001pt; font-size:11.0pt; font-family:"Calibri",sans-serif;} a:link, span.MsoHyperlink {mso-style-priority:99; color:blue; text-decoration:underline;} a:visited, span.MsoHyperlinkFollowed {mso-style-priority:99; color:purple; text-decoration:underline;} p.msonormal0, li.msonormal0, div.msonormal0 {mso-style-name:msonormal; mso-margin-top-alt:auto; margin-right:0cm; mso-margin-bottom-alt:auto; margin-left:0cm; font-size:11.0pt; font-family:"Calibri",sans-serif;} span.EmailStyle19 {mso-style-type:personal-reply; font-family:"Calibri",sans-serif; color:windowtext;} .MsoChpDefault {mso-style-type:export-only; font-size:10.0pt;} @page WordSection1 {size:612.0pt 792.0pt; margin:72.0pt 72.0pt 72.0pt 72.0pt;} div.WordSection1 {page:WordSection1;} --></style> </head> <body lang="EN-GB" link="blue" vlink="purple"> <div class="WordSection1"> <p class="MsoNormal">This problem has been solved – see our TYPES 2018 abstract (attached). <o:p></o:p></p> <p class="MsoNormal"><o:p> </o:p></p> <p class="MsoNormal">Basically the idea is to define a relation between “pre-terms” and the semantics and then show that this is contractible for “well-typed objects”, this way you avoid the mutual dependency. This was an idea by Andras Kovacs. In this year’s TYPES there are two abstracts that show how this can be used to give a universal reduction from Inductive-Inductive types to indexed inductive types and hence W-types. <o:p></o:p></p> <p class="MsoNormal"><o:p> </o:p></p> <p class="MsoNormal">I have discussed this with Jesper when he was in Nottingham and I think our tentative conclusion was that this could be combined with his approach to provide a reduction for IITs. However, this needs to be checked.<o:p></o:p></p> <p class="MsoNormal"><o:p> </o:p></p> <p class="MsoNormal">Thorsten<o:p></o:p></p> <p class="MsoNormal"><o:p> </o:p></p> <div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm"> <p class="MsoNormal" style="margin-left:36.0pt"><b><span style="font-size:12.0pt;color:black">From: </span></b><span style="font-size:12.0pt;color:black"><homotopytypetheory@googlegroups.com> on behalf of Matt Oliveri <atmacen@gmail.com><br> <b>Date: </b>Tuesday, 21 May 2019 at 01:28<br> <b>To: </b>Homotopy Type Theory <homotopytypetheory@googlegroups.com><br> <b>Subject: </b>Re: [HoTT] Semantics of QIITs ?<o:p></o:p></span></p> </div> <div> <p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p> </div> <div> <p class="MsoNormal" style="margin-left:36.0pt">I'm not completely satisfied with Hugunin's technique, because it justifies only the "simple" elimination principle, rather than the general, "recursive-recursive" elimination principle implemented in Agda. As far as I can tell, realistic use cases for inductive-inductive families also need the recursive-recursive elimination principle, where the types of the maps out of later families depend on the maps out of earlier families. (I'm not sure how much of the other research on IIFs stops short of handling recursion-recursion, but I think it should be taken seriously.)<br> <br> On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote: <o:p></o:p></p> <blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm"> <p class="MsoNormal" style="margin-left:36.0pt">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 :) <br> <br> Best, <br> Jon<o:p></o:p></p> </blockquote> </div> <p class="MsoNormal" style="margin-left:36.0pt">-- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com?utm_medium=email&utm_source=footer"> https://groups.google.com/d/msgid/HomotopyTypeTheory/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com</a>.<br> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br> <br> <o:p></o:p></p> </div> <PRE> 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. </PRE></body> </html> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/3DC3F379-F057-49AF-9232-CDC925E9646B%40nottingham.ac.uk?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/3DC3F379-F057-49AF-9232-CDC925E9646B%40nottingham.ac.uk</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br /> [-- Attachment #2: main.pdf --] [-- Type: application/pdf, Size: 313696 bytes --]

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.

[-- 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 --] <div dir="ltr">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.<div><br></div><div>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.</div><div><br></div><div>Are there any other examples in the HoTT book?</div><div><br></div><div>Best,</div><div>Andrew<br><br>On Thursday, 16 May 2019 16:57:36 UTC+2, Bas Spitters wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">What is the status of the semantics of quotient inductive inductive types? <br>Looking at the literature there's some progress on reducing QIITs to <br>simpler constructions, but this does not seem to have led to a <br>convenient semantic result. <br>E.g. QIITs do not seem to be treated in the work by Lumdaine and Shulman. <br> <br><a href="https://ncatlab.org/nlab/show/inductive-inductive+type" target="_blank" rel="nofollow" onmousedown="this.href='https://www.google.com/url?q\x3dhttps%3A%2F%2Fncatlab.org%2Fnlab%2Fshow%2Finductive-inductive%2Btype\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNHAbFjGcCbrwRtJ-YChHPAQu-ah6w';return true;" onclick="this.href='https://www.google.com/url?q\x3dhttps%3A%2F%2Fncatlab.org%2Fnlab%2Fshow%2Finductive-inductive%2Btype\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNHAbFjGcCbrwRtJ-YChHPAQu-ah6w';return true;">https://ncatlab.org/nlab/show/<wbr>inductive-inductive+type</a> <br> <br>Do we know that the prototypical QIITs from the book (e.g. Cauchy <br>reals) are supported in the usual models of HoTT? <br> <br>Thanks, <br> <br>Bas <br></blockquote></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/f580d237-12b5-4107-92c4-7738fd89e59f%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/f580d237-12b5-4107-92c4-7738fd89e59f%40googlegroups.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

Thanks. Yes, if we have CAC and set-quotients things simplify. Of course, the reason to use QIITs is precisely to have a more general treatment when CAC is not available. On Tue, May 21, 2019 at 1:47 PM Andrew Swan <wakelin.swan@gmail.com> wrote: > > 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. -- 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/CAOoPQuTWGc04i%2BcwOFaGLDuD8_b_53hR%3DXRZ7UmHo8-fjO6zOw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 2905 bytes --] Thanks. This sounds a lot like the interpreter I did (https://homotopytypetheory.org/2014/08/19/a-formalized-interpreter/) that required UIP, and like Streicher's method for proving initiality of the syntax of dependent type theory. Combining it with Hugunin's technique sounds promising! On Tuesday, May 21, 2019 at 4:33:10 AM UTC-4, Thorsten Altenkirch wrote: > > This problem has been solved – see our TYPES 2018 abstract (attached). > > > > Basically the idea is to define a relation between “pre-terms” and the > semantics and then show that this is contractible for “well-typed objects”, > this way you avoid the mutual dependency. This was an idea by Andras > Kovacs. In this year’s TYPES there are two abstracts that show how this can > be used to give a universal reduction from Inductive-Inductive types to > indexed inductive types and hence W-types. > > > > I have discussed this with Jesper when he was in Nottingham and I think > our tentative conclusion was that this could be combined with his approach > to provide a reduction for IITs. However, this needs to be checked. > > > > Thorsten > > > > *From: *<homotopyt...@googlegroups.com <javascript:>> on behalf of Matt > Oliveri <atm...@gmail.com <javascript:>> > *Date: *Tuesday, 21 May 2019 at 01:28 > *To: *Homotopy Type Theory <homotopyt...@googlegroups.com <javascript:>> > *Subject: *Re: [HoTT] Semantics of QIITs ? > > > > I'm not completely satisfied with Hugunin's technique, because it > justifies only the "simple" elimination principle, rather than the general, > "recursive-recursive" elimination principle implemented in Agda. As far as > I can tell, realistic use cases for inductive-inductive families also need > the recursive-recursive elimination principle, where the types of the maps > out of later families depend on the maps out of earlier families. (I'm not > sure how much of the other research on IIFs stops short of handling > recursion-recursion, but I think it should be taken seriously.) > > On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote: > > 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 > > > -- 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/22a97b80-cab0-49f6-b3fb-b1b44fd41e9c%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 4801 bytes --] <div dir="ltr">Thanks. This sounds a lot like the interpreter I did (https://homotopytypetheory.org/2014/08/19/a-formalized-interpreter/) that required UIP, and like Streicher's method for proving initiality of the syntax of dependent type theory. Combining it with Hugunin's technique sounds promising!<br><br>On Tuesday, May 21, 2019 at 4:33:10 AM UTC-4, Thorsten Altenkirch wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"> <div link="blue" vlink="purple" lang="EN-GB"> <div> <p class="MsoNormal">This problem has been solved – see our TYPES 2018 abstract (attached). </p> <p class="MsoNormal"> </p> <p class="MsoNormal">Basically the idea is to define a relation between “pre-terms” and the semantics and then show that this is contractible for “well-typed objects”, this way you avoid the mutual dependency. This was an idea by Andras Kovacs. In this year’s TYPES there are two abstracts that show how this can be used to give a universal reduction from Inductive-Inductive types to indexed inductive types and hence W-types. </p> <p class="MsoNormal"> </p> <p class="MsoNormal">I have discussed this with Jesper when he was in Nottingham and I think our tentative conclusion was that this could be combined with his approach to provide a reduction for IITs. However, this needs to be checked.</p> <p class="MsoNormal"> </p> <p class="MsoNormal">Thorsten</p> <p class="MsoNormal"> </p> <div style="border:none;border-top:solid #b5c4df 1.0pt;padding:3.0pt 0cm 0cm 0cm"> <p class="MsoNormal" style="margin-left:36.0pt"><b><span style="font-size:12.0pt;color:black">From: </span></b><span style="font-size:12.0pt;color:black"><<a href="javascript:" target="_blank" gdf-obfuscated-mailto="Yl6LmecLAwAJ" rel="nofollow" onmousedown="this.href='javascript:';return true;" onclick="this.href='javascript:';return true;">homotopyt...@<wbr>googlegroups.com</a>> on behalf of Matt Oliveri <<a href="javascript:" target="_blank" gdf-obfuscated-mailto="Yl6LmecLAwAJ" rel="nofollow" onmousedown="this.href='javascript:';return true;" onclick="this.href='javascript:';return true;">atm...@gmail.com</a>><br> <b>Date: </b>Tuesday, 21 May 2019 at 01:28<br> <b>To: </b>Homotopy Type Theory <<a href="javascript:" target="_blank" gdf-obfuscated-mailto="Yl6LmecLAwAJ" rel="nofollow" onmousedown="this.href='javascript:';return true;" onclick="this.href='javascript:';return true;">homotopyt...@<wbr>googlegroups.com</a>><br> <b>Subject: </b>Re: [HoTT] Semantics of QIITs ?</span></p> </div> <div> <p class="MsoNormal" style="margin-left:36.0pt"> </p> </div> <div> <p class="MsoNormal" style="margin-left:36.0pt">I'm not completely satisfied with Hugunin's technique, because it justifies only the "simple" elimination principle, rather than the general, "recursive-recursive" elimination principle implemented in Agda. As far as I can tell, realistic use cases for inductive-inductive families also need the recursive-recursive elimination principle, where the types of the maps out of later families depend on the maps out of earlier families. (I'm not sure how much of the other research on IIFs stops short of handling recursion-recursion, but I think it should be taken seriously.)<br> <br> On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote: </p> <blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm"> <p class="MsoNormal" style="margin-left:36.0pt">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 :) <br> <br> Best, <br> Jon</p> </blockquote> </div><br></div></div> </blockquote></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/22a97b80-cab0-49f6-b3fb-b1b44fd41e9c%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/22a97b80-cab0-49f6-b3fb-b1b44fd41e9c%40googlegroups.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />