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