```Discussion of Homotopy Type Theory and Univalent Foundations
help / color / mirror / Atom feed```
```* Re: [HoTT] Infinitary type theory
@ 2023-01-27 20:40 ` Jason Gross
2023-01-28 15:21   ` Nicolai Kraus
From: Jason Gross @ 2023-01-27 20:40 UTC (permalink / raw)

[-- Attachment #1: Type: text/plain, Size: 4725 bytes --]

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
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
> 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 --]

```* Re: [HoTT] Infinitary type theory
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
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.

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
> 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
>> 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
> To view this discussion on the web visit
> .
>

--
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 --]

```* Re: [HoTT] Infinitary type theory
2023-01-28 15:21   ` Nicolai Kraus
@ 2023-01-28 17:45     ` Michael Shulman
2023-01-28 20:26       ` Jason Gross
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.

```* Re: [HoTT] Infinitary type theory
2023-01-28 17:45     ` Michael Shulman
@ 2023-01-28 20:26       ` Jason Gross
2023-01-29 11:38         ` András Kovács
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,
> 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
> >>> 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
> >> To view this discussion on the web visit
> .
>

--
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 --]

```* Re: [HoTT] Infinitary type theory
2023-01-28 20:26       ` Jason Gross
@ 2023-01-29 11:38         ` András Kovács
2023-01-31  1:11           ` Jason Gross
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,
>> 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
>> >> To view this discussion on the web visit
>> .
>>
> --
> 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
> To view this discussion on the web visit
> .
>

--
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 --]

```* Re: [HoTT] Infinitary type theory
2023-01-29 11:38         ` András Kovács
@ 2023-01-31  1:11           ` Jason Gross
0 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,
>>> 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
>>> .
>>>
>> --
>> 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
>> To view this discussion on the web visit
>> .
>>
>

--
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 --]

```end of thread, other threads:[~2023-01-31  1:12 UTC | newest]

```This is a public inbox, see mirroring instructions