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