From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 15655 invoked from network); 28 Jan 2023 20:26:33 -0000 Received: from mail-pg1-x53f.google.com (2607:f8b0:4864:20::53f) by inbox.vuxu.org with ESMTPUTF8; 28 Jan 2023 20:26:33 -0000 Received: by mail-pg1-x53f.google.com with SMTP id q130-20020a632a88000000b004a03cfb3ac6sf3238044pgq.6 for ; Sat, 28 Jan 2023 12:26:33 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1674937592; cv=pass; d=google.com; s=arc-20160816; b=EXoCPON5fcnL+MAIlSieH2pe3Rqn+Oh0TfxGMoKqEO8d5Azxu2f7ZzF2YVsmCZ+LrP xBamFyVtcDnjd/Vu77F+PjX2Jxs7BPEEqwJTdBLD/jeQEn+C3v6F5HX6I4F4eRoxDHQm US6ycdV8l6rv+Uduy2DX2JmWqZOmbGADRJwCKwTmn36GTFbpUMaMgkCAzKTgSVzyZu6L xVZeMOoHcb7bDONRuaNS2Mu8f8a5/KqDgNFAVMipf35hfuZOG3dKRl8Nbu5/zu3GN+LA a5kxQoSgp/sPcv2yMKT0fyNNX6odOE/lO72rzlO5NRd1mN0rNnJxCIIoMy3YE9peepLq jiGQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=gebYA9SaSQdgm1ip0qdRfOHVX3Q1BHyKHzhA23INI1k=; b=t0OuudDexTi6lhiHmK1sv0uFo/pQL7q+SVBjLYjaUjQKyrL3LyeB1hGpdjXso560pX w9yzQdzLMeKb3PAdjZPkSSCQRXUzlnGnJFl+C57IEwMtXFSoteK8nWWZw44ln8TdyUxh vaDq7VTWzc+QdEdosthJpuQHvWNI8VKMBQDZ5ouSL8QPndtMRFncemI1pKOtdUyXizLz OzxZhKrWSOe/M2FP9ehuB9GZVKcDADLx8jc9ynU1dRsDTbtpXuB+mOI40BJ1HtQoWBkp 68TEfyqhiYrr4B+JfnZf/AC5xBLQkV8LkLY74MlriUVIX884RRX5jMr1G8Wx7i1Q/vxj Lt6A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=j1ESvMGR; spf=pass (google.com: domain of jasongross9@gmail.com designates 2001:4860:4864:20::2d as permitted sender) smtp.mailfrom=jasongross9@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=gebYA9SaSQdgm1ip0qdRfOHVX3Q1BHyKHzhA23INI1k=; b=ZdDPeSNEfFoq5+3bYVitCxRiYQRJsHN9n01blCVNUCGUKcE7sTeK6Ca88YB8Oo81Sj F+hIPIYe+YH1G9Xeeiv6XZI+gESmV9ARPHEepCo86kwpzCkOOeZPKRReCHfNalEm2pzM Lz8U5P1TKYNGk4cDbHfdwro+3g7SVBNooQQkrcgrb6FyknrdFOhs1kwJz46V7drLsRWQ 28HB1VKv3uwqYWyXxVmomGB6l0vy/xjam63D/90WgKmJettB1tgJ1V51zTcYlhfnXS+P HWBTnBDWd6MHM2DQCU6cSjCs0ZZvCmyBGmY7CgvqSIcGSrjpaSp+Out8JyArmr8dyyQN s2oQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:from:to:cc:subject:date:message-id:reply-to; bh=gebYA9SaSQdgm1ip0qdRfOHVX3Q1BHyKHzhA23INI1k=; b=Cm/lw/O7t52bVOU/YKHAHkXrgh9FcF13NMeAR24UZxGiruxct+bWXtFyJ9KjuZ1cCL jaYhZvj77AEjA846amvdqjiuKGUhRghxCSqQijrL4l338RVzxrxPofUSkqSk34dZe+mP yWNr5QraJiTyLe2QmHpjZZ0TIeMcVIRG+qtZTgrTkBjH4ALmxHsmlBStOm8xqYZ1TfG5 4YPdyqJEMI3ql1SQ8mOkPxI0iP0VLH0mWT5BQhPjehNBUbV/WsCD35FrmYDsyiXYZdhY kbi5/hfrlKCGkHIGIPDoulxAh5wfDGtM0pFpPB3GkxQhH+9lEh3rpwNmU2pNv42tE/3J rGiA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=gebYA9SaSQdgm1ip0qdRfOHVX3Q1BHyKHzhA23INI1k=; b=mTaqGLiRRLWRYcCSxTyKWXrkbq81RAky+bOj6+JDGHH1lU4tXZ0K/WCtfShGtxWbCy m6vPoMTDlDvWkOKCUQWNX8zpZOqOPnFDXQ4d2RWmiCO9++wglTy3FFDmOgLy5u0vv7+X w07wC9Iwqn6muNK9G888yadDALcAzxYOgn5fxUcpVroGOYf6E7v/Ss74Ac24D8TFHYJN 3g86Z2ojOiXNJhJ8kMg9leT5S5QRryhJxNo1DXfGO3lCECuFTr3g1pUxaKSINkptyReQ IQxGo9RiEDItdyMrOJnTYTtRT7kV/5ONyhx+dD69m6rbek3he87xUUD9KEFJ8wXGsbUv Cj6A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AO0yUKXyNFjI0bQapprjVHkvkUV0Ye8/vwfKl3WmW+dVQHY342kM3ZfH zWcnEYk/zg5V8Ahv7XhDd18= X-Google-Smtp-Source: AK7set8yLMhOWnZFL480viqSto6fXqIly0HKgLZpTXfDrejr3oQT2mHYb8+C/v0QtlIkz+2X3zzmlQ== X-Received: by 2002:a63:5a62:0:b0:4de:eb5f:ea9c with SMTP id k34-20020a635a62000000b004deeb5fea9cmr1191169pgm.0.1674937591472; Sat, 28 Jan 2023 12:26:31 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:a3c2:b0:192:62df:a3e7 with SMTP id q2-20020a170902a3c200b0019262dfa3e7ls8376918plb.9.-pod-prod-gmail; Sat, 28 Jan 2023 12:26:29 -0800 (PST) X-Received: by 2002:a17:902:bf03:b0:194:9847:9cd4 with SMTP id bi3-20020a170902bf0300b0019498479cd4mr40209047plb.60.1674937589634; Sat, 28 Jan 2023 12:26:29 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1674937589; cv=none; d=google.com; s=arc-20160816; b=FQCOGwSMSHirNvA7Q51ZY/acVd2Gbntgc6YiJgrw0mMto2NUti4nGHLL8pYG28E1Om 0589W/xZX/ML5bmWyjGrx0Q8Vx+NHQno0YtC8Z5wzIZasKlZz71ZlZFtn4DqOC5cDKXz U5UypRg8AtANLxsr5JytMGlx+xFwg/qCK1BmKKoPOfILbSxTPPxBjySTgSNyqgD33ZQz QZi+jL1Y5TkvOfSqj+eF7QGpSJl42KVDKJMF17/ibreuWtCo59nrk3jgyUlM3REmFDqA FYdTLeassDvxawMdU2+vwTcOLDvxXtrX62HPiUvlqER7QjAvETbRny8N+HZhR2aVtxTX o4uA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=U61oCbI6T5RwnxBe7TbUx/8cLjZ1QYRYcQfsOEPK4TA=; b=ve0MsNE7JHrF7iPjb6yeo4Y7wPjzFGutQibICR7u9sw8b6rG9t/PNSYoYPaX/0P0V5 fCyl/qibaClwiRiog9YcT/cO9go2bi+d+dlGweP5KkBRvXfBB5tds+cMdPS/AzwZwpA2 x5XUHgRdSajcnm9LL9zG9pp4SlQotXOFi60PaYGaB4LOHwccup/GqstB1XrDzvNU0rMj k/UrnpvSV3NC179MQN9X7Ek0clixuIh6ymkTSnpD/3KwlYyHu4cPRiRM4sjEYTjAEVNq JGMJJmySGQE54Jp0TuJAModY3V5ANUFTzTJe7+Hwh/tURThJNpkQ+966lAZvflabFIM6 +o/A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=j1ESvMGR; spf=pass (google.com: domain of jasongross9@gmail.com designates 2001:4860:4864:20::2d as permitted sender) smtp.mailfrom=jasongross9@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-oa1-x2d.google.com (mail-oa1-x2d.google.com. [2001:4860:4864:20::2d]) by gmr-mx.google.com with ESMTPS id d4-20020a170903230400b00185499dcc29si257284plh.7.2023.01.28.12.26.29 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 28 Jan 2023 12:26:29 -0800 (PST) Received-SPF: pass (google.com: domain of jasongross9@gmail.com designates 2001:4860:4864:20::2d as permitted sender) client-ip=2001:4860:4864:20::2d; Received: by mail-oa1-x2d.google.com with SMTP id 586e51a60fabf-12c8312131fso10692579fac.4 for ; Sat, 28 Jan 2023 12:26:29 -0800 (PST) X-Received: by 2002:a05:6871:b301:b0:157:f67d:1614 with SMTP id bd1-20020a056871b30100b00157f67d1614mr3598543oac.234.1674937588809; Sat, 28 Jan 2023 12:26:28 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Jason Gross Date: Sat, 28 Jan 2023 15:26:17 -0500 Message-ID: Subject: Re: [HoTT] Infinitary type theory To: Michael Shulman Cc: Nicolai Kraus , "HomotopyTypeTheory@googlegroups.com" Content-Type: multipart/alternative; boundary="00000000000000848605f358ccae" X-Original-Sender: JasonGross9@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=j1ESvMGR; spf=pass (google.com: domain of jasongross9@gmail.com designates 2001:4860:4864:20::2d as permitted sender) smtp.mailfrom=jasongross9@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , --00000000000000848605f358ccae Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > 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 "=CE=BB 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 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 > 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 inheren= t > consequence of infinitary constructors. I'd rather say that it's an > accidental side effect of Mike's formulation from 2014 that something lik= e > "=CE=BB i. Type i" is possible, and it can easily be ruled out. In Sectio= n 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 index= ed > sequence of types still has to live in a single fixed universe. > > > > Agda actually *does* allow something like "=CE=BB i. Type i". While I v= iew > 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 fou= nd > it very useful. Without something like this, I don't see how we could hav= e > formalised the statement that "Universe Un is not an n-type in a hierarch= y > 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-Complicate= dTypes.html > > > > Best wishes, > > Nicolai > > > > > > > > On Fri, Jan 27, 2023 at 8:41 PM Jason Gross > 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 `=E2=96=A1A` to mean "syntax for A", an infi= nitary > type theory has rules like `(A =E2=86=92 =E2=96=A1B) =E2=86=92 =E2=96=A1(= A =E2=86=92 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 (conside= r > the function `=CE=BB i. "Type"=E1=B5=A2`). 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 <=3D i <=3D 1" into terms that use universes between 0= and 2 > (because we have enough universes to do that), and then we can embed term= s > with universes between 0 and 2 back into terms with universes between 0 a= nd > 1 (divide universe indices by 2), and this loop gives inconsistency by > G=C3=B6del / L=C3=B6b. > >> > >> 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 > 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 ha= s > >>> 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 o= f > >>> 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 term= s > >>> 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, sen= d > 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/CAKObCarzP9wE1t2Y8M7= Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com > . > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3Q= A%40mail.gmail.com. --00000000000000848605f358ccae Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
> I don't think access to internal universe quanti= fications is an inherent consequence of infinitary constructors. I'd ra= ther say that it's an accidental side effect of Mike's formulation = from 2014 that something like "=CE=BB 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 specifi= ed without allowing internal universe quantification. This is essentially b= ecause the externally indexed sequence of types still has to live in a sing= le fixed universe.

As I unders= tand it, this just rules out universe qualification that is not bounded abo= ve by a fixed universe, right?=C2=A0 It seems to me that you still get inte= rnal quantization over levels less than a fixed level.=C2=A0 And this is en= ough to make the construction generating inconsistency with Q-indexed unive= rses go through.

On Sat, Jan 28, 2023, 12:46 Michael Shulman <shulman@sandiego.edu> wrote:
<= /div>
Also, apparently Agda's Set-omega b= reaks 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 o= f universe hierarchies is orthogonal to the question of infinitary type con= structors.
>
> I don't think access to internal universe quantifications is an in= herent consequence of infinitary constructors. I'd rather say that it&#= 39;s an accidental side effect of Mike's formulation from 2014 that som= ething like "=CE=BB 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 allowin= g internal universe quantification. This is essentially because the externa= lly indexed sequence of types still has to live in a single fixed universe.=
>
> Agda actually *does* allow something like "=CE=BB 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 thi= s, I don't see how we could have formalised the statement that "Un= iverse Un is not an n-type in a hierarchy U0, U1, U2, ... of univalent univ= erses (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 i= sn't even part of the considered type theory) that it can be implemente= d.
>
> [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-Complica= tedTypes.html
>
> Best wishes,
> Nicolai
>
>
>
> On Fri, Jan 27, 2023 at 8:41 PM Jason Gross <jasongross9@gmail.c= om> wrote:
>>
>> (Resurrecting this thread because I stumbled upon it while rereadi= ng A Formalized Interpreter, and I believe I have something new to add.) >>
>> As I understand it, using `=E2=96=A1A` to mean "syntax for A&= quot;, an infinitary type theory has rules like `(A =E2=86=92 =E2=96=A1B) = =E2=86=92 =E2=96=A1(A =E2=86=92 B)`.=C2=A0 (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".=C2=A0 In &qu= ot;An Order-Theoretic Analysis of Universe Polymorphism", Favonia, Car= lo Angiuli, and Reed Mullanix have a consistency proof for a system with ra= tional-indexed universes (and no explicit universe level quantification).= =C2=A0 However, infinitary rules give access to internal universe quantific= ation (consider the function `=CE=BB i. "Type"=E1=B5=A2`).=C2=A0 = I believe HOAS-like internal-level quantification rules out any "fract= al-like" scheme of universes (such as the rationals), because we can w= rite an interpreter for "terms using universes i with 0 <=3D i <= =3D 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 be= tween 0 and 2 back into terms with universes between 0 and 1 (divide univer= se indices by 2), and this loop gives inconsistency by G=C3=B6del / L=C3=B6= b.
>>
>> So at the very least, having infinitary limits rules out some of t= he more exotic universe level structures.
>>
>> Best,
>> Jason
>>
>>
>> On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sand= iego.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, w= hich has
>>> been kicking around in my head for a while.=C2=A0 I know that = something
>>> similar has occurred to others as well.
>>>
>>> Logicians study infinitary logics in addition to finitary ones= .=C2=A0 Why
>>> can't we have an infinitary type theory?
>>>
>>> An infinitary type theory would include type-forming operation= s which
>>> take infinitely many inputs ("infinite" in the sense= of the
>>> metatheory).=C2=A0 The most obvious would be, say, the cartesi= an product of
>>> infinitely many types, e.g. given types A0, A1, A2, ... (with = the
>>> indexing being by external natural numbers), we would have a t= ype
>>> Prod_i(Ai), and so on.=C2=A0 Semantically, this would correspo= nd to a
>>> category having infinite products.
>>>
>>> More useful than this would be a category having limits of tow= ers of
>>> fibrations.=C2=A0 I think this can be represented as a type fo= rmer 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.=C2=A0 We might also ne= ed an
>>> "infinitary extensionality" axiom.
>>>
>>> It seems that in such a type theory, we ought to have no troub= le
>>> defining (say) semisimplicial types, as the limit of the appro= priate
>>> externally-defined tower of fibrations.
>>>
>>> Has anyone studied infinitary type theories before?=C2=A0 Of c= ourse, they
>>> probably won't have all the good properties of finitary on= es.=C2=A0 For
>>> instance, I think judgmental equality isn't going to be de= cidable,
>>> since there's no way to algorithmically test the infinitel= y many terms
>>> that go into a lam_i for equality.=C2=A0 But other proposals l= ike HTS are
>>> also giving up decidability.=C2=A0 Are there other more seriou= s problems
>>> with an infinitary type theory?
>>>
>>> Mike
>>>
>>> --
>>> You received this message because you are subscribed to the Go= ogle Groups "Homotopy Type Theory" group.
>>> To unsubscribe from this group and stop receiving emails from = it, send an email to HomotopyTypeTheory+unsu= bscribe@googlegroups.com.
>>> For more options, visit https://groups.goo= gle.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+unsubscr= ibe@googlegroups.com.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t= 2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https= ://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaoJMQhY5upSKXTM%3DLHE= 72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.com.
--00000000000000848605f358ccae--