*Re: [HoTT] Infinitary type theory[not found] <CAOvivQwi8jXfY6Vx7yrQoBmwj6id8xsPC6fX+8j74cq4V7e+Ug@mail.gmail.com>@ 2023-01-27 20:40 ` Jason Gross2023-01-28 15:21 ` Nicolai Kraus 0 siblings, 1 reply; 6+ messages in thread From: Jason Gross @ 2023-01-27 20:40 UTC (permalink / raw) To: Michael Shulman;+Cc:HomotopyTypeTheory@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 4725 bytes --] (Resurrecting this thread because I stumbled upon it while rereading A Formalized Interpreter <https://homotopytypetheory.org/2014/08/19/a-formalized-interpreter/>, and I believe I have something new to add.) As I understand it, using `□A` to mean "syntax for A", an infinitary type theory has rules like `(A → □B) → □(A → B)`. (Note that this is exactly what HOAS does, which explains why it's so easy to write an interpreter for HOAS without running into the semisimplicial types coherence issues.) > Are there other more serious problems with an infinitary type theory? I think the answer to this is "it depends". In "An Order-Theoretic Analysis of Universe Polymorphism" <https://favonia.org/files/mugen.pdf>, Favonia, Carlo Angiuli, and Reed Mullanix have a consistency proof for a system with rational-indexed universes (and no explicit universe level quantification). However, infinitary rules give access to internal universe quantification (consider the function `λ i. "Type"ᵢ`). I believe HOAS-like internal-level quantification rules out any "fractal-like" scheme of universes (such as the rationals), because we can write an interpreter for "terms using universes i with 0 <= i <= 1" into terms that use universes between 0 and 2 (because we have enough universes to do that), and then we can embed terms with universes between 0 and 2 back into terms with universes between 0 and 1 (divide universe indices by 2), and this loop gives inconsistency by Gödel / Löb. So at the very least, having infinitary limits rules out some of the more exotic universe level structures. Best, Jason On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sandiego.edu> wrote: > Since the problem of defining infinite structures has come up in > another thread, it may be a good time to bring up this idea, which has > been kicking around in my head for a while. I know that something > similar has occurred to others as well. > > Logicians study infinitary logics in addition to finitary ones. Why > can't we have an infinitary type theory? > > An infinitary type theory would include type-forming operations which > take infinitely many inputs ("infinite" in the sense of the > metatheory). The most obvious would be, say, the cartesian product of > infinitely many types, e.g. given types A0, A1, A2, ... (with the > indexing being by external natural numbers), we would have a type > Prod_i(Ai), and so on. Semantically, this would correspond to a > category having infinite products. > > More useful than this would be a category having limits of towers of > fibrations. I think this can be represented as a type former in an > infinitary type theory as well, with a rule like > > Gamma |- A0 : Type > Gamma, a0:A0 |- A1(a0) : Type > Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type > Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type > ... > ---------------------------------------- > Gamma |- lim_i A_i : Type > > Then we would have a corresponding introduction form, like > > Gamma |- x0 : A0 > Gamma |- x1 : A1(x0) > Gamma |- x2 : A1(x0,x1) > ... > ------------------------------------- > Gamma |- lam_i xi : lim_i A_i > > with elimination and computation rules. We might also need an > "infinitary extensionality" axiom. > > It seems that in such a type theory, we ought to have no trouble > defining (say) semisimplicial types, as the limit of the appropriate > externally-defined tower of fibrations. > > Has anyone studied infinitary type theories before? Of course, they > probably won't have all the good properties of finitary ones. For > instance, I think judgmental equality isn't going to be decidable, > since there's no way to algorithmically test the infinitely many terms > that go into a lam_i for equality. But other proposals like HTS are > also giving up decidability. Are there other more serious problems > with an infinitary type theory? > > Mike > > -- > 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. > 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/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 5945 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [HoTT] Infinitary type theory2023-01-27 20:40 ` [HoTT] Infinitary type theory Jason Gross@ 2023-01-28 15:21 ` Nicolai Kraus2023-01-28 17:45 ` Michael Shulman 0 siblings, 1 reply; 6+ messages in thread From: Nicolai Kraus @ 2023-01-28 15:21 UTC (permalink / raw) To: Jason Gross;+Cc:Michael Shulman, HomotopyTypeTheory@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 7160 bytes --] That's an interesting observation! However, I think the question of universe hierarchies is orthogonal to the question of infinitary type constructors. I don't think access to internal universe quantifications is an inherent consequence of infinitary constructors. I'd rather say that it's an accidental side effect of Mike's formulation from 2014 that something like "λ i. Type i" is possible, and it can easily be ruled out. In Section 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such infinitary type constructors is specified without allowing internal universe quantification. This is essentially because the externally indexed sequence of types still has to live in a single fixed universe. Agda actually *does* allow something like "λ i. Type i". While I view constructions using it more as proof schemes than as single proofs ("book HoTT" wouldn't allow it, you'll have to fix an index), I occasionally found it very useful. Without something like this, I don't see how we could have formalised the statement that "Universe Un is not an n-type in a hierarchy U0, U1, U2, ... of univalent universes (without HITs)" [2]. But I would *not* regard the formalisation [3] as a single proof. I see it as an externally indexed family of Nat-many proofs, and it's only a lucky accident (using a feature of Agda that isn't even part of the considered type theory) that it can be implemented. [1] https://arxiv.org/abs/1705.03307 [2] https://arxiv.org/abs/1311.4002 [3] https://www.cs.nott.ac.uk/~psznk/docs/thesisagda_nicolai/HHHUU-ComplicatedTypes.html Best wishes, Nicolai On Fri, Jan 27, 2023 at 8:41 PM Jason Gross <jasongross9@gmail.com> wrote: > (Resurrecting this thread because I stumbled upon it while rereading A > Formalized Interpreter > <https://homotopytypetheory.org/2014/08/19/a-formalized-interpreter/>, > and I believe I have something new to add.) > > As I understand it, using `□A` to mean "syntax for A", an infinitary type > theory has rules like `(A → □B) → □(A → B)`. (Note that this is exactly > what HOAS does, which explains why it's so easy to write an interpreter for > HOAS without running into the semisimplicial types coherence issues.) > > > Are there other more serious problems with an infinitary type theory? > I think the answer to this is "it depends". In "An Order-Theoretic > Analysis of Universe Polymorphism" <https://favonia.org/files/mugen.pdf>, > Favonia, Carlo Angiuli, and Reed Mullanix have a consistency proof for a > system with rational-indexed universes (and no explicit universe level > quantification). However, infinitary rules give access to internal > universe quantification (consider the function `λ i. "Type"ᵢ`). I believe > HOAS-like internal-level quantification rules out any "fractal-like" scheme > of universes (such as the rationals), because we can write an interpreter > for "terms using universes i with 0 <= i <= 1" into terms that use > universes between 0 and 2 (because we have enough universes to do that), > and then we can embed terms with universes between 0 and 2 back into terms > with universes between 0 and 1 (divide universe indices by 2), and this > loop gives inconsistency by Gödel / Löb. > > So at the very least, having infinitary limits rules out some of the more > exotic universe level structures. > > Best, > Jason > > > On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sandiego.edu> > wrote: > >> Since the problem of defining infinite structures has come up in >> another thread, it may be a good time to bring up this idea, which has >> been kicking around in my head for a while. I know that something >> similar has occurred to others as well. >> >> Logicians study infinitary logics in addition to finitary ones. Why >> can't we have an infinitary type theory? >> >> An infinitary type theory would include type-forming operations which >> take infinitely many inputs ("infinite" in the sense of the >> metatheory). The most obvious would be, say, the cartesian product of >> infinitely many types, e.g. given types A0, A1, A2, ... (with the >> indexing being by external natural numbers), we would have a type >> Prod_i(Ai), and so on. Semantically, this would correspond to a >> category having infinite products. >> >> More useful than this would be a category having limits of towers of >> fibrations. I think this can be represented as a type former in an >> infinitary type theory as well, with a rule like >> >> Gamma |- A0 : Type >> Gamma, a0:A0 |- A1(a0) : Type >> Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type >> Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type >> ... >> ---------------------------------------- >> Gamma |- lim_i A_i : Type >> >> Then we would have a corresponding introduction form, like >> >> Gamma |- x0 : A0 >> Gamma |- x1 : A1(x0) >> Gamma |- x2 : A1(x0,x1) >> ... >> ------------------------------------- >> Gamma |- lam_i xi : lim_i A_i >> >> with elimination and computation rules. We might also need an >> "infinitary extensionality" axiom. >> >> It seems that in such a type theory, we ought to have no trouble >> defining (say) semisimplicial types, as the limit of the appropriate >> externally-defined tower of fibrations. >> >> Has anyone studied infinitary type theories before? Of course, they >> probably won't have all the good properties of finitary ones. For >> instance, I think judgmental equality isn't going to be decidable, >> since there's no way to algorithmically test the infinitely many terms >> that go into a lam_i for equality. But other proposals like HTS are >> also giving up decidability. Are there other more serious problems >> with an infinitary type theory? >> >> Mike >> >> -- >> 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. >> 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/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CA%2BAZBBqyc%3DyjbeNbcmdWRXnyyBzaUu3G1x2Mp5cdZA8Asg5oLQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 9061 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [HoTT] Infinitary type theory2023-01-28 15:21 ` Nicolai Kraus@ 2023-01-28 17:45 ` Michael Shulman2023-01-28 20:26 ` Jason Gross 0 siblings, 1 reply; 6+ messages in thread From: Michael Shulman @ 2023-01-28 17:45 UTC (permalink / raw) To: Nicolai Kraus;+Cc:Jason Gross, HomotopyTypeTheory@googlegroups.com Also, apparently Agda's Set-omega breaks subject reduction: https://github.com/agda/agda/issues/5810 On Sat, Jan 28, 2023 at 7:21 AM Nicolai Kraus <nicolai.kraus@gmail.com> wrote: > > That's an interesting observation! However, I think the question of universe hierarchies is orthogonal to the question of infinitary type constructors. > > I don't think access to internal universe quantifications is an inherent consequence of infinitary constructors. I'd rather say that it's an accidental side effect of Mike's formulation from 2014 that something like "λ i. Type i" is possible, and it can easily be ruled out. In Section 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such infinitary type constructors is specified without allowing internal universe quantification. This is essentially because the externally indexed sequence of types still has to live in a single fixed universe. > > Agda actually *does* allow something like "λ i. Type i". While I view constructions using it more as proof schemes than as single proofs ("book HoTT" wouldn't allow it, you'll have to fix an index), I occasionally found it very useful. Without something like this, I don't see how we could have formalised the statement that "Universe Un is not an n-type in a hierarchy U0, U1, U2, ... of univalent universes (without HITs)" [2]. But I would *not* regard the formalisation [3] as a single proof. I see it as an externally indexed family of Nat-many proofs, and it's only a lucky accident (using a feature of Agda that isn't even part of the considered type theory) that it can be implemented. > > [1] https://arxiv.org/abs/1705.03307 > [2] https://arxiv.org/abs/1311.4002 > [3] https://www.cs.nott.ac.uk/~psznk/docs/thesisagda_nicolai/HHHUU-ComplicatedTypes.html > > Best wishes, > Nicolai > > > > On Fri, Jan 27, 2023 at 8:41 PM Jason Gross <jasongross9@gmail.com> wrote: >> >> (Resurrecting this thread because I stumbled upon it while rereading A Formalized Interpreter, and I believe I have something new to add.) >> >> As I understand it, using `□A` to mean "syntax for A", an infinitary type theory has rules like `(A → □B) → □(A → B)`. (Note that this is exactly what HOAS does, which explains why it's so easy to write an interpreter for HOAS without running into the semisimplicial types coherence issues.) >> >> > Are there other more serious problems with an infinitary type theory? >> I think the answer to this is "it depends". In "An Order-Theoretic Analysis of Universe Polymorphism", Favonia, Carlo Angiuli, and Reed Mullanix have a consistency proof for a system with rational-indexed universes (and no explicit universe level quantification). However, infinitary rules give access to internal universe quantification (consider the function `λ i. "Type"ᵢ`). I believe HOAS-like internal-level quantification rules out any "fractal-like" scheme of universes (such as the rationals), because we can write an interpreter for "terms using universes i with 0 <= i <= 1" into terms that use universes between 0 and 2 (because we have enough universes to do that), and then we can embed terms with universes between 0 and 2 back into terms with universes between 0 and 1 (divide universe indices by 2), and this loop gives inconsistency by Gödel / Löb. >> >> So at the very least, having infinitary limits rules out some of the more exotic universe level structures. >> >> Best, >> Jason >> >> >> On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sandiego.edu> wrote: >>> >>> Since the problem of defining infinite structures has come up in >>> another thread, it may be a good time to bring up this idea, which has >>> been kicking around in my head for a while. I know that something >>> similar has occurred to others as well. >>> >>> Logicians study infinitary logics in addition to finitary ones. Why >>> can't we have an infinitary type theory? >>> >>> An infinitary type theory would include type-forming operations which >>> take infinitely many inputs ("infinite" in the sense of the >>> metatheory). The most obvious would be, say, the cartesian product of >>> infinitely many types, e.g. given types A0, A1, A2, ... (with the >>> indexing being by external natural numbers), we would have a type >>> Prod_i(Ai), and so on. Semantically, this would correspond to a >>> category having infinite products. >>> >>> More useful than this would be a category having limits of towers of >>> fibrations. I think this can be represented as a type former in an >>> infinitary type theory as well, with a rule like >>> >>> Gamma |- A0 : Type >>> Gamma, a0:A0 |- A1(a0) : Type >>> Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type >>> Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type >>> ... >>> ---------------------------------------- >>> Gamma |- lim_i A_i : Type >>> >>> Then we would have a corresponding introduction form, like >>> >>> Gamma |- x0 : A0 >>> Gamma |- x1 : A1(x0) >>> Gamma |- x2 : A1(x0,x1) >>> ... >>> ------------------------------------- >>> Gamma |- lam_i xi : lim_i A_i >>> >>> with elimination and computation rules. We might also need an >>> "infinitary extensionality" axiom. >>> >>> It seems that in such a type theory, we ought to have no trouble >>> defining (say) semisimplicial types, as the limit of the appropriate >>> externally-defined tower of fibrations. >>> >>> Has anyone studied infinitary type theories before? Of course, they >>> probably won't have all the good properties of finitary ones. For >>> instance, I think judgmental equality isn't going to be decidable, >>> since there's no way to algorithmically test the infinitely many terms >>> that go into a lam_i for equality. But other proposals like HTS are >>> also giving up decidability. Are there other more serious problems >>> with an infinitary type theory? >>> >>> Mike >>> >>> -- >>> 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. >>> 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/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com. -- 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/CADYavpypv0OieLCmivNYHYf7f8VnN1zWaKbafO-EP7kkPxg1dA%40mail.gmail.com. ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [HoTT] Infinitary type theory2023-01-28 17:45 ` Michael Shulman@ 2023-01-28 20:26 ` Jason Gross2023-01-29 11:38 ` András Kovács 0 siblings, 1 reply; 6+ messages in thread From: Jason Gross @ 2023-01-28 20:26 UTC (permalink / raw) To: Michael Shulman;+Cc:Nicolai Kraus, HomotopyTypeTheory@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 8403 bytes --] > I don't think access to internal universe quantifications is an inherent consequence of infinitary constructors. I'd rather say that it's an accidental side effect of Mike's formulation from 2014 that something like "λ i. Type i" is possible, and it can easily be ruled out. In Section 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such infinitary type constructors is specified without allowing internal universe quantification. This is essentially because the externally indexed sequence of types still has to live in a single fixed universe. As I understand it, this just rules out universe qualification that is not bounded above by a fixed universe, right? It seems to me that you still get internal quantization over levels less than a fixed level. And this is enough to make the construction generating inconsistency with Q-indexed universes go through. On Sat, Jan 28, 2023, 12:46 Michael Shulman <shulman@sandiego.edu> wrote: > Also, apparently Agda's Set-omega breaks subject reduction: > https://github.com/agda/agda/issues/5810 > > On Sat, Jan 28, 2023 at 7:21 AM Nicolai Kraus <nicolai.kraus@gmail.com> > wrote: > > > > That's an interesting observation! However, I think the question of > universe hierarchies is orthogonal to the question of infinitary type > constructors. > > > > I don't think access to internal universe quantifications is an inherent > consequence of infinitary constructors. I'd rather say that it's an > accidental side effect of Mike's formulation from 2014 that something like > "λ i. Type i" is possible, and it can easily be ruled out. In Section 2.4, > strengthening A1-3 of the 2LTT paper [1], a type theory with such > infinitary type constructors is specified without allowing internal > universe quantification. This is essentially because the externally indexed > sequence of types still has to live in a single fixed universe. > > > > Agda actually *does* allow something like "λ i. Type i". While I view > constructions using it more as proof schemes than as single proofs ("book > HoTT" wouldn't allow it, you'll have to fix an index), I occasionally found > it very useful. Without something like this, I don't see how we could have > formalised the statement that "Universe Un is not an n-type in a hierarchy > U0, U1, U2, ... of univalent universes (without HITs)" [2]. But I would > *not* regard the formalisation [3] as a single proof. I see it as an > externally indexed family of Nat-many proofs, and it's only a lucky > accident (using a feature of Agda that isn't even part of the considered > type theory) that it can be implemented. > > > > [1] https://arxiv.org/abs/1705.03307 > > [2] https://arxiv.org/abs/1311.4002 > > [3] > https://www.cs.nott.ac.uk/~psznk/docs/thesisagda_nicolai/HHHUU-ComplicatedTypes.html > > > > Best wishes, > > Nicolai > > > > > > > > On Fri, Jan 27, 2023 at 8:41 PM Jason Gross <jasongross9@gmail.com> > wrote: > >> > >> (Resurrecting this thread because I stumbled upon it while rereading A > Formalized Interpreter, and I believe I have something new to add.) > >> > >> As I understand it, using `□A` to mean "syntax for A", an infinitary > type theory has rules like `(A → □B) → □(A → B)`. (Note that this is > exactly what HOAS does, which explains why it's so easy to write an > interpreter for HOAS without running into the semisimplicial types > coherence issues.) > >> > >> > Are there other more serious problems with an infinitary type theory? > >> I think the answer to this is "it depends". In "An Order-Theoretic > Analysis of Universe Polymorphism", Favonia, Carlo Angiuli, and Reed > Mullanix have a consistency proof for a system with rational-indexed > universes (and no explicit universe level quantification). However, > infinitary rules give access to internal universe quantification (consider > the function `λ i. "Type"ᵢ`). I believe HOAS-like internal-level > quantification rules out any "fractal-like" scheme of universes (such as > the rationals), because we can write an interpreter for "terms using > universes i with 0 <= i <= 1" into terms that use universes between 0 and 2 > (because we have enough universes to do that), and then we can embed terms > with universes between 0 and 2 back into terms with universes between 0 and > 1 (divide universe indices by 2), and this loop gives inconsistency by > Gödel / Löb. > >> > >> So at the very least, having infinitary limits rules out some of the > more exotic universe level structures. > >> > >> Best, > >> Jason > >> > >> > >> On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sandiego.edu> > wrote: > >>> > >>> Since the problem of defining infinite structures has come up in > >>> another thread, it may be a good time to bring up this idea, which has > >>> been kicking around in my head for a while. I know that something > >>> similar has occurred to others as well. > >>> > >>> Logicians study infinitary logics in addition to finitary ones. Why > >>> can't we have an infinitary type theory? > >>> > >>> An infinitary type theory would include type-forming operations which > >>> take infinitely many inputs ("infinite" in the sense of the > >>> metatheory). The most obvious would be, say, the cartesian product of > >>> infinitely many types, e.g. given types A0, A1, A2, ... (with the > >>> indexing being by external natural numbers), we would have a type > >>> Prod_i(Ai), and so on. Semantically, this would correspond to a > >>> category having infinite products. > >>> > >>> More useful than this would be a category having limits of towers of > >>> fibrations. I think this can be represented as a type former in an > >>> infinitary type theory as well, with a rule like > >>> > >>> Gamma |- A0 : Type > >>> Gamma, a0:A0 |- A1(a0) : Type > >>> Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type > >>> Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type > >>> ... > >>> ---------------------------------------- > >>> Gamma |- lim_i A_i : Type > >>> > >>> Then we would have a corresponding introduction form, like > >>> > >>> Gamma |- x0 : A0 > >>> Gamma |- x1 : A1(x0) > >>> Gamma |- x2 : A1(x0,x1) > >>> ... > >>> ------------------------------------- > >>> Gamma |- lam_i xi : lim_i A_i > >>> > >>> with elimination and computation rules. We might also need an > >>> "infinitary extensionality" axiom. > >>> > >>> It seems that in such a type theory, we ought to have no trouble > >>> defining (say) semisimplicial types, as the limit of the appropriate > >>> externally-defined tower of fibrations. > >>> > >>> Has anyone studied infinitary type theories before? Of course, they > >>> probably won't have all the good properties of finitary ones. For > >>> instance, I think judgmental equality isn't going to be decidable, > >>> since there's no way to algorithmically test the infinitely many terms > >>> that go into a lam_i for equality. But other proposals like HTS are > >>> also giving up decidability. Are there other more serious problems > >>> with an infinitary type theory? > >>> > >>> Mike > >>> > >>> -- > >>> 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. > >>> 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/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com > . > -- 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/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 11155 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [HoTT] Infinitary type theory2023-01-28 20:26 ` Jason Gross@ 2023-01-29 11:38 ` András Kovács2023-01-31 1:11 ` Jason Gross 0 siblings, 1 reply; 6+ messages in thread From: András Kovács @ 2023-01-29 11:38 UTC (permalink / raw) To: Jason Gross Cc: Michael Shulman, Nicolai Kraus, HomotopyTypeTheory@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 9852 bytes --] Jason: I agree that externally indexed products imply bounded universe polymorphism, but I don't understand how we can derive inconsistency from that together with rational levels. The operation that scales rational levels can only be defined externally so it doesn't really affect the possible internal constructions. To be clear, by external products I mean e.g. the following for i : ℚ Product : (ℕ → Tyᵢ Γ) → Tyᵢ Γ lam : ((n : ℕ) → Tmᵢ Γ (A n)) → Tmᵢ Γ (Product A) app : Tmᵢ Γ (Product A) → (n : ℕ) → Tmᵢ Γ (A n) Jason Gross <jasongross9@gmail.com> ezt írta (időpont: 2023. jan. 28., Szo, 21:26): > > I don't think access to internal universe quantifications is an inherent > consequence of infinitary constructors. I'd rather say that it's an > accidental side effect of Mike's formulation from 2014 that something like > "λ i. Type i" is possible, and it can easily be ruled out. In Section 2.4, > strengthening A1-3 of the 2LTT paper [1], a type theory with such > infinitary type constructors is specified without allowing internal > universe quantification. This is essentially because the externally indexed > sequence of types still has to live in a single fixed universe. > > As I understand it, this just rules out universe qualification that is not > bounded above by a fixed universe, right? It seems to me that you still > get internal quantization over levels less than a fixed level. And this is > enough to make the construction generating inconsistency with Q-indexed > universes go through. > > On Sat, Jan 28, 2023, 12:46 Michael Shulman <shulman@sandiego.edu> wrote: > >> Also, apparently Agda's Set-omega breaks subject reduction: >> https://github.com/agda/agda/issues/5810 >> >> On Sat, Jan 28, 2023 at 7:21 AM Nicolai Kraus <nicolai.kraus@gmail.com> >> wrote: >> > >> > That's an interesting observation! However, I think the question of >> universe hierarchies is orthogonal to the question of infinitary type >> constructors. >> > >> > I don't think access to internal universe quantifications is an >> inherent consequence of infinitary constructors. I'd rather say that it's >> an accidental side effect of Mike's formulation from 2014 that something >> like "λ i. Type i" is possible, and it can easily be ruled out. In Section >> 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such >> infinitary type constructors is specified without allowing internal >> universe quantification. This is essentially because the externally indexed >> sequence of types still has to live in a single fixed universe. >> > >> > Agda actually *does* allow something like "λ i. Type i". While I view >> constructions using it more as proof schemes than as single proofs ("book >> HoTT" wouldn't allow it, you'll have to fix an index), I occasionally found >> it very useful. Without something like this, I don't see how we could have >> formalised the statement that "Universe Un is not an n-type in a hierarchy >> U0, U1, U2, ... of univalent universes (without HITs)" [2]. But I would >> *not* regard the formalisation [3] as a single proof. I see it as an >> externally indexed family of Nat-many proofs, and it's only a lucky >> accident (using a feature of Agda that isn't even part of the considered >> type theory) that it can be implemented. >> > >> > [1] https://arxiv.org/abs/1705.03307 >> > [2] https://arxiv.org/abs/1311.4002 >> > [3] >> https://www.cs.nott.ac.uk/~psznk/docs/thesisagda_nicolai/HHHUU-ComplicatedTypes.html >> > >> > Best wishes, >> > Nicolai >> > >> > >> > >> > On Fri, Jan 27, 2023 at 8:41 PM Jason Gross <jasongross9@gmail.com> >> wrote: >> >> >> >> (Resurrecting this thread because I stumbled upon it while rereading A >> Formalized Interpreter, and I believe I have something new to add.) >> >> >> >> As I understand it, using `□A` to mean "syntax for A", an infinitary >> type theory has rules like `(A → □B) → □(A → B)`. (Note that this is >> exactly what HOAS does, which explains why it's so easy to write an >> interpreter for HOAS without running into the semisimplicial types >> coherence issues.) >> >> >> >> > Are there other more serious problems with an infinitary type theory? >> >> I think the answer to this is "it depends". In "An Order-Theoretic >> Analysis of Universe Polymorphism", Favonia, Carlo Angiuli, and Reed >> Mullanix have a consistency proof for a system with rational-indexed >> universes (and no explicit universe level quantification). However, >> infinitary rules give access to internal universe quantification (consider >> the function `λ i. "Type"ᵢ`). I believe HOAS-like internal-level >> quantification rules out any "fractal-like" scheme of universes (such as >> the rationals), because we can write an interpreter for "terms using >> universes i with 0 <= i <= 1" into terms that use universes between 0 and 2 >> (because we have enough universes to do that), and then we can embed terms >> with universes between 0 and 2 back into terms with universes between 0 and >> 1 (divide universe indices by 2), and this loop gives inconsistency by >> Gödel / Löb. >> >> >> >> So at the very least, having infinitary limits rules out some of the >> more exotic universe level structures. >> >> >> >> Best, >> >> Jason >> >> >> >> >> >> On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sandiego.edu> >> wrote: >> >>> >> >>> Since the problem of defining infinite structures has come up in >> >>> another thread, it may be a good time to bring up this idea, which has >> >>> been kicking around in my head for a while. I know that something >> >>> similar has occurred to others as well. >> >>> >> >>> Logicians study infinitary logics in addition to finitary ones. Why >> >>> can't we have an infinitary type theory? >> >>> >> >>> An infinitary type theory would include type-forming operations which >> >>> take infinitely many inputs ("infinite" in the sense of the >> >>> metatheory). The most obvious would be, say, the cartesian product of >> >>> infinitely many types, e.g. given types A0, A1, A2, ... (with the >> >>> indexing being by external natural numbers), we would have a type >> >>> Prod_i(Ai), and so on. Semantically, this would correspond to a >> >>> category having infinite products. >> >>> >> >>> More useful than this would be a category having limits of towers of >> >>> fibrations. I think this can be represented as a type former in an >> >>> infinitary type theory as well, with a rule like >> >>> >> >>> Gamma |- A0 : Type >> >>> Gamma, a0:A0 |- A1(a0) : Type >> >>> Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type >> >>> Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type >> >>> ... >> >>> ---------------------------------------- >> >>> Gamma |- lim_i A_i : Type >> >>> >> >>> Then we would have a corresponding introduction form, like >> >>> >> >>> Gamma |- x0 : A0 >> >>> Gamma |- x1 : A1(x0) >> >>> Gamma |- x2 : A1(x0,x1) >> >>> ... >> >>> ------------------------------------- >> >>> Gamma |- lam_i xi : lim_i A_i >> >>> >> >>> with elimination and computation rules. We might also need an >> >>> "infinitary extensionality" axiom. >> >>> >> >>> It seems that in such a type theory, we ought to have no trouble >> >>> defining (say) semisimplicial types, as the limit of the appropriate >> >>> externally-defined tower of fibrations. >> >>> >> >>> Has anyone studied infinitary type theories before? Of course, they >> >>> probably won't have all the good properties of finitary ones. For >> >>> instance, I think judgmental equality isn't going to be decidable, >> >>> since there's no way to algorithmically test the infinitely many terms >> >>> that go into a lam_i for equality. But other proposals like HTS are >> >>> also giving up decidability. Are there other more serious problems >> >>> with an infinitary type theory? >> >>> >> >>> Mike >> >>> >> >>> -- >> >>> 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. >> >>> 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/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com >> . >> > -- > 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/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CAA3CDBYe%2BOnZedPWdVNLKJKfWwM77gVe_-7v4WmU%3DwQd17EkdA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 12958 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread

*2023-01-29 11:38 ` András KovácsRe: [HoTT] Infinitary type theory@ 2023-01-31 1:11 ` Jason Gross0 siblings, 0 replies; 6+ messages in thread From: Jason Gross @ 2023-01-31 1:11 UTC (permalink / raw) To: András Kovács Cc: Michael Shulman, Nicolai Kraus, HomotopyTypeTheory@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 10342 bytes --] Ah, you're right, sorry. I was confusing "being able to name particular universes as function outputs" with "bounded universe polymorphism". I retract my claim. Best, Jason On Sun, Jan 29, 2023 at 6:38 AM András Kovács <puttamalac@gmail.com> wrote: > Jason: I agree that externally indexed products imply bounded universe > polymorphism, but I don't understand how we can derive inconsistency from > that together with rational levels. The operation that scales rational > levels can only be defined externally so it doesn't really affect the > possible internal constructions. > > To be clear, by external products I mean e.g. the following for i : ℚ > > Product : (ℕ → Tyᵢ Γ) → Tyᵢ Γ > lam : ((n : ℕ) → Tmᵢ Γ (A n)) → Tmᵢ Γ (Product A) > app : Tmᵢ Γ (Product A) → (n : ℕ) → Tmᵢ Γ (A n) > > Jason Gross <jasongross9@gmail.com> ezt írta (időpont: 2023. jan. 28., > Szo, 21:26): > >> > I don't think access to internal universe quantifications is an >> inherent consequence of infinitary constructors. I'd rather say that it's >> an accidental side effect of Mike's formulation from 2014 that something >> like "λ i. Type i" is possible, and it can easily be ruled out. In Section >> 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such >> infinitary type constructors is specified without allowing internal >> universe quantification. This is essentially because the externally indexed >> sequence of types still has to live in a single fixed universe. >> >> As I understand it, this just rules out universe qualification that is >> not bounded above by a fixed universe, right? It seems to me that you >> still get internal quantization over levels less than a fixed level. And >> this is enough to make the construction generating inconsistency with >> Q-indexed universes go through. >> >> On Sat, Jan 28, 2023, 12:46 Michael Shulman <shulman@sandiego.edu> wrote: >> >>> Also, apparently Agda's Set-omega breaks subject reduction: >>> https://github.com/agda/agda/issues/5810 >>> >>> On Sat, Jan 28, 2023 at 7:21 AM Nicolai Kraus <nicolai.kraus@gmail.com> >>> wrote: >>> > >>> > That's an interesting observation! However, I think the question of >>> universe hierarchies is orthogonal to the question of infinitary type >>> constructors. >>> > >>> > I don't think access to internal universe quantifications is an >>> inherent consequence of infinitary constructors. I'd rather say that it's >>> an accidental side effect of Mike's formulation from 2014 that something >>> like "λ i. Type i" is possible, and it can easily be ruled out. In Section >>> 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such >>> infinitary type constructors is specified without allowing internal >>> universe quantification. This is essentially because the externally indexed >>> sequence of types still has to live in a single fixed universe. >>> > >>> > Agda actually *does* allow something like "λ i. Type i". While I view >>> constructions using it more as proof schemes than as single proofs ("book >>> HoTT" wouldn't allow it, you'll have to fix an index), I occasionally found >>> it very useful. Without something like this, I don't see how we could have >>> formalised the statement that "Universe Un is not an n-type in a hierarchy >>> U0, U1, U2, ... of univalent universes (without HITs)" [2]. But I would >>> *not* regard the formalisation [3] as a single proof. I see it as an >>> externally indexed family of Nat-many proofs, and it's only a lucky >>> accident (using a feature of Agda that isn't even part of the considered >>> type theory) that it can be implemented. >>> > >>> > [1] https://arxiv.org/abs/1705.03307 >>> > [2] https://arxiv.org/abs/1311.4002 >>> > [3] >>> https://www.cs.nott.ac.uk/~psznk/docs/thesisagda_nicolai/HHHUU-ComplicatedTypes.html >>> > >>> > Best wishes, >>> > Nicolai >>> > >>> > >>> > >>> > On Fri, Jan 27, 2023 at 8:41 PM Jason Gross <jasongross9@gmail.com> >>> wrote: >>> >> >>> >> (Resurrecting this thread because I stumbled upon it while rereading >>> A Formalized Interpreter, and I believe I have something new to add.) >>> >> >>> >> As I understand it, using `□A` to mean "syntax for A", an infinitary >>> type theory has rules like `(A → □B) → □(A → B)`. (Note that this is >>> exactly what HOAS does, which explains why it's so easy to write an >>> interpreter for HOAS without running into the semisimplicial types >>> coherence issues.) >>> >> >>> >> > Are there other more serious problems with an infinitary type >>> theory? >>> >> I think the answer to this is "it depends". In "An Order-Theoretic >>> Analysis of Universe Polymorphism", Favonia, Carlo Angiuli, and Reed >>> Mullanix have a consistency proof for a system with rational-indexed >>> universes (and no explicit universe level quantification). However, >>> infinitary rules give access to internal universe quantification (consider >>> the function `λ i. "Type"ᵢ`). I believe HOAS-like internal-level >>> quantification rules out any "fractal-like" scheme of universes (such as >>> the rationals), because we can write an interpreter for "terms using >>> universes i with 0 <= i <= 1" into terms that use universes between 0 and 2 >>> (because we have enough universes to do that), and then we can embed terms >>> with universes between 0 and 2 back into terms with universes between 0 and >>> 1 (divide universe indices by 2), and this loop gives inconsistency by >>> Gödel / Löb. >>> >> >>> >> So at the very least, having infinitary limits rules out some of the >>> more exotic universe level structures. >>> >> >>> >> Best, >>> >> Jason >>> >> >>> >> >>> >> On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sandiego.edu> >>> wrote: >>> >>> >>> >>> Since the problem of defining infinite structures has come up in >>> >>> another thread, it may be a good time to bring up this idea, which >>> has >>> >>> been kicking around in my head for a while. I know that something >>> >>> similar has occurred to others as well. >>> >>> >>> >>> Logicians study infinitary logics in addition to finitary ones. Why >>> >>> can't we have an infinitary type theory? >>> >>> >>> >>> An infinitary type theory would include type-forming operations which >>> >>> take infinitely many inputs ("infinite" in the sense of the >>> >>> metatheory). The most obvious would be, say, the cartesian product >>> of >>> >>> infinitely many types, e.g. given types A0, A1, A2, ... (with the >>> >>> indexing being by external natural numbers), we would have a type >>> >>> Prod_i(Ai), and so on. Semantically, this would correspond to a >>> >>> category having infinite products. >>> >>> >>> >>> More useful than this would be a category having limits of towers of >>> >>> fibrations. I think this can be represented as a type former in an >>> >>> infinitary type theory as well, with a rule like >>> >>> >>> >>> Gamma |- A0 : Type >>> >>> Gamma, a0:A0 |- A1(a0) : Type >>> >>> Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type >>> >>> Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type >>> >>> ... >>> >>> ---------------------------------------- >>> >>> Gamma |- lim_i A_i : Type >>> >>> >>> >>> Then we would have a corresponding introduction form, like >>> >>> >>> >>> Gamma |- x0 : A0 >>> >>> Gamma |- x1 : A1(x0) >>> >>> Gamma |- x2 : A1(x0,x1) >>> >>> ... >>> >>> ------------------------------------- >>> >>> Gamma |- lam_i xi : lim_i A_i >>> >>> >>> >>> with elimination and computation rules. We might also need an >>> >>> "infinitary extensionality" axiom. >>> >>> >>> >>> It seems that in such a type theory, we ought to have no trouble >>> >>> defining (say) semisimplicial types, as the limit of the appropriate >>> >>> externally-defined tower of fibrations. >>> >>> >>> >>> Has anyone studied infinitary type theories before? Of course, they >>> >>> probably won't have all the good properties of finitary ones. For >>> >>> instance, I think judgmental equality isn't going to be decidable, >>> >>> since there's no way to algorithmically test the infinitely many >>> terms >>> >>> that go into a lam_i for equality. But other proposals like HTS are >>> >>> also giving up decidability. Are there other more serious problems >>> >>> with an infinitary type theory? >>> >>> >>> >>> Mike >>> >>> >>> >>> -- >>> >>> 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. >>> >>> 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/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com >>> . >>> >> -- >> 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/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.com >> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/CAKObCaoZUnvTfEOPdX8nwOUZM_M%3DnEoszZYizE4%2BypoymDLozQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 13688 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread

end of thread, other threads:[~2023-01-31 1:12 UTC | newest]Thread overview:6+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- [not found] <CAOvivQwi8jXfY6Vx7yrQoBmwj6id8xsPC6fX+8j74cq4V7e+Ug@mail.gmail.com> 2023-01-27 20:40 ` [HoTT] Infinitary type theory Jason Gross 2023-01-28 15:21 ` Nicolai Kraus 2023-01-28 17:45 ` Michael Shulman 2023-01-28 20:26 ` Jason Gross 2023-01-29 11:38 ` András Kovács 2023-01-31 1:11 ` Jason Gross

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).