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