* [HoTT] Semantics of QIITs ? @ 2019-05-16 14:57 Bas Spitters 2019-05-16 15:39 ` Thorsten Altenkirch 2019-05-21 11:47 ` [HoTT] " Andrew Swan 0 siblings, 2 replies; 19+ messages in thread From: Bas Spitters @ 2019-05-16 14:57 UTC (permalink / raw) To: homotopytypetheory 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-16 14:57 [HoTT] Semantics of QIITs ? Bas Spitters @ 2019-05-16 15:39 ` Thorsten Altenkirch 2019-05-16 15:50 ` Bas Spitters 2019-05-21 11:47 ` [HoTT] " Andrew Swan 1 sibling, 1 reply; 19+ messages in thread From: Thorsten Altenkirch @ 2019-05-16 15:39 UTC (permalink / raw) To: Bas Spitters, homotopytypetheory; +Cc: Ambrus Kaposi, Kovács András 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-16 15:39 ` Thorsten Altenkirch @ 2019-05-16 15:50 ` Bas Spitters 2019-05-16 16:15 ` András Kovács 0 siblings, 1 reply; 19+ messages in thread From: Bas Spitters @ 2019-05-16 15:50 UTC (permalink / raw) To: Thorsten Altenkirch Cc: homotopytypetheory, Ambrus Kaposi, Kovács András 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-16 15:50 ` Bas Spitters @ 2019-05-16 16:15 ` András Kovács 2019-05-16 18:50 ` Bas Spitters 0 siblings, 1 reply; 19+ messages in thread From: András Kovács @ 2019-05-16 16:15 UTC (permalink / raw) To: Bas Spitters; +Cc: Thorsten Altenkirch, homotopytypetheory, Ambrus Kaposi [-- 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 --] ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-16 16:15 ` András Kovács @ 2019-05-16 18:50 ` Bas Spitters 2019-05-20 16:16 ` Thorsten Altenkirch 0 siblings, 1 reply; 19+ messages in thread From: Bas Spitters @ 2019-05-16 18:50 UTC (permalink / raw) To: András Kovács Cc: Thorsten Altenkirch, homotopytypetheory, Ambrus Kaposi 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-16 18:50 ` Bas Spitters @ 2019-05-20 16:16 ` Thorsten Altenkirch 2019-05-20 17:54 ` Bas Spitters 0 siblings, 1 reply; 19+ messages in thread From: Thorsten Altenkirch @ 2019-05-20 16:16 UTC (permalink / raw) To: Bas Spitters, András Kovács; +Cc: homotopytypetheory, Ambrus Kaposi 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-20 16:16 ` Thorsten Altenkirch @ 2019-05-20 17:54 ` Bas Spitters 2019-05-20 18:35 ` Thorsten Altenkirch 0 siblings, 1 reply; 19+ messages in thread From: Bas Spitters @ 2019-05-20 17:54 UTC (permalink / raw) To: Thorsten Altenkirch Cc: András Kovács, homotopytypetheory, Ambrus Kaposi 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-20 17:54 ` Bas Spitters @ 2019-05-20 18:35 ` Thorsten Altenkirch 2019-05-20 19:59 ` Jon Sterling 0 siblings, 1 reply; 19+ messages in thread From: Thorsten Altenkirch @ 2019-05-20 18:35 UTC (permalink / raw) To: Bas Spitters; +Cc: András Kovács, homotopytypetheory, Ambrus Kaposi 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-20 18:35 ` Thorsten Altenkirch @ 2019-05-20 19:59 ` Jon Sterling 2019-05-20 21:04 ` Bas Spitters 0 siblings, 1 reply; 19+ messages in thread From: Jon Sterling @ 2019-05-20 19:59 UTC (permalink / raw) To: 'Martin Escardo' via Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-20 19:59 ` Jon Sterling @ 2019-05-20 21:04 ` Bas Spitters 2019-05-20 22:17 ` Thorsten Altenkirch 0 siblings, 1 reply; 19+ messages in thread From: Bas Spitters @ 2019-05-20 21:04 UTC (permalink / raw) To: Jon Sterling; +Cc: 'Martin Escardo' via Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-20 21:04 ` Bas Spitters @ 2019-05-20 22:17 ` Thorsten Altenkirch 2019-05-20 23:26 ` Jon Sterling 0 siblings, 1 reply; 19+ messages in thread From: Thorsten Altenkirch @ 2019-05-20 22:17 UTC (permalink / raw) To: Bas Spitters Cc: Jon Sterling, 'Martin Escardo' via Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-20 22:17 ` Thorsten Altenkirch @ 2019-05-20 23:26 ` Jon Sterling 2019-05-21 0:28 ` Matt Oliveri 2019-05-21 8:39 ` Thorsten Altenkirch 0 siblings, 2 replies; 19+ messages in thread From: Jon Sterling @ 2019-05-20 23:26 UTC (permalink / raw) To: 'Martin Escardo' via Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-20 23:26 ` Jon Sterling @ 2019-05-21 0:28 ` Matt Oliveri 2019-05-21 2:45 ` Jasper Hugunin 2019-05-21 8:33 ` Thorsten Altenkirch 2019-05-21 8:39 ` Thorsten Altenkirch 1 sibling, 2 replies; 19+ messages in thread From: Matt Oliveri @ 2019-05-21 0:28 UTC (permalink / raw) To: Homotopy Type Theory [-- 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 --] ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-21 0:28 ` Matt Oliveri @ 2019-05-21 2:45 ` Jasper Hugunin 2019-05-21 8:33 ` Thorsten Altenkirch 1 sibling, 0 replies; 19+ messages in thread From: Jasper Hugunin @ 2019-05-21 2:45 UTC (permalink / raw) To: HomotopyTypeTheory [-- 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 --] ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-21 0:28 ` Matt Oliveri 2019-05-21 2:45 ` Jasper Hugunin @ 2019-05-21 8:33 ` Thorsten Altenkirch 2019-05-21 19:56 ` Matt Oliveri 1 sibling, 1 reply; 19+ messages in thread From: Thorsten Altenkirch @ 2019-05-21 8:33 UTC (permalink / raw) To: Matt Oliveri, Homotopy Type Theory [-- 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 --] [-- Attachment #2: main.pdf --] [-- Type: application/pdf, Size: 313696 bytes --] ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-21 8:33 ` Thorsten Altenkirch @ 2019-05-21 19:56 ` Matt Oliveri 0 siblings, 0 replies; 19+ messages in thread From: Matt Oliveri @ 2019-05-21 19:56 UTC (permalink / raw) To: Homotopy Type Theory [-- 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 --] ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Semantics of QIITs ? 2019-05-20 23:26 ` Jon Sterling 2019-05-21 0:28 ` Matt Oliveri @ 2019-05-21 8:39 ` Thorsten Altenkirch 1 sibling, 0 replies; 19+ messages in thread From: Thorsten Altenkirch @ 2019-05-21 8:39 UTC (permalink / raw) To: Jon Sterling, 'Martin Escardo' via Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
* [HoTT] Re: Semantics of QIITs ? 2019-05-16 14:57 [HoTT] Semantics of QIITs ? Bas Spitters 2019-05-16 15:39 ` Thorsten Altenkirch @ 2019-05-21 11:47 ` Andrew Swan 2019-05-21 12:14 ` Bas Spitters 1 sibling, 1 reply; 19+ messages in thread From: Andrew Swan @ 2019-05-21 11:47 UTC (permalink / raw) To: Homotopy Type Theory [-- 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 --] ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: [HoTT] Re: Semantics of QIITs ? 2019-05-21 11:47 ` [HoTT] " Andrew Swan @ 2019-05-21 12:14 ` Bas Spitters 0 siblings, 0 replies; 19+ messages in thread From: Bas Spitters @ 2019-05-21 12:14 UTC (permalink / raw) To: Andrew Swan; +Cc: Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 19+ messages in thread
end of thread, other threads:[~2019-05-21 19:56 UTC | newest] Thread overview: 19+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2019-05-16 14:57 [HoTT] Semantics of QIITs ? Bas Spitters 2019-05-16 15:39 ` Thorsten Altenkirch 2019-05-16 15:50 ` Bas Spitters 2019-05-16 16:15 ` András Kovács 2019-05-16 18:50 ` Bas Spitters 2019-05-20 16:16 ` Thorsten Altenkirch 2019-05-20 17:54 ` Bas Spitters 2019-05-20 18:35 ` Thorsten Altenkirch 2019-05-20 19:59 ` Jon Sterling 2019-05-20 21:04 ` Bas Spitters 2019-05-20 22:17 ` Thorsten Altenkirch 2019-05-20 23:26 ` Jon Sterling 2019-05-21 0:28 ` Matt Oliveri 2019-05-21 2:45 ` Jasper Hugunin 2019-05-21 8:33 ` Thorsten Altenkirch 2019-05-21 19:56 ` Matt Oliveri 2019-05-21 8:39 ` Thorsten Altenkirch 2019-05-21 11:47 ` [HoTT] " Andrew Swan 2019-05-21 12:14 ` Bas Spitters
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).