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 2255 invoked from network); 29 Jan 2023 11:38:45 -0000 Received: from mail-pl1-x638.google.com (2607:f8b0:4864:20::638) by inbox.vuxu.org with ESMTPUTF8; 29 Jan 2023 11:38:45 -0000 Received: by mail-pl1-x638.google.com with SMTP id p15-20020a170902a40f00b00192b2bbb7f8sf5017203plq.14 for ; Sun, 29 Jan 2023 03:38:45 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1674992324; cv=pass; d=google.com; s=arc-20160816; b=UGzmyl9RlOgDY0AXzmJpJitUOPg0IPEa56+3TNz5ao/bzuLtzXbz/+xuEC2wVxsGYP x6Ziw9dKOZELZVV3LqDqDq07IeQz58wefM2u8Y8dcE83vwozCVzMHAH8IA7OrbVMnsNA Kr9bzOzOTM1Y+gp2fLjgo3Ft1MfNBozt0THqhBCCj9NSXNwxEInk4xkTM6243hvmCZ5Z YPxxmqFEYkX34XP7cVREgIxElDE9m8PUPtEOrzflB3oh8ILkjVJXEtDEuOnjyXpZmM6L XukubinKoKb6F/FgUsJTtbDnsC/Kk63BfPQrlm6RbbV8xNK+2aYf0edQ0v4XLaduEXL2 WQ6g== 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=EIvic+Vew3fa5py89fJxZi5y2z9HPkKVZsFlcgXlCEs=; b=Qqzt7KOonArWfJEU8HWk2vbWJ8WpynETrMTbuD8rJP3tVjQB3tGFjfP40G6rNFL2/B BpUujqgZb7UfBVsTN7v9piCXeEcQFL7yTGcAs57Qz1Sx0Vlq8vQ6HjgD24IOxL2we1jZ wBgC10dMTpGBP+PgonFY+YiU2oI2LPPCW5m4bpZialS1L7xHxP/s+iVcCFG7yXDWbI0Y uZiJnym5TgajG/8adPSvN4252vaFwdfHr51JY7dD6y6vLw0CHetsgOxME77x2XlEuB/o t26xwK698u7Goi+DH2ix5I2xTJEvjN0js8YZyhbOh9lTJRUktR7EwAWLd8Bt4b4BSDR7 TiSw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=HPQR4kbo; spf=pass (google.com: domain of puttamalac@gmail.com designates 2607:f8b0:4864:20::a2e as permitted sender) smtp.mailfrom=puttamalac@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=EIvic+Vew3fa5py89fJxZi5y2z9HPkKVZsFlcgXlCEs=; b=AkuxlJFqjoq0MnqJ+mxhNYLH/s0rpjMmqHrGL952gYZou+xsH1ZDaEFPXxLRx+ZAdO +VLER9QLHmWJ3E1kpSFzlsSb3sdajvVE4V+CxZ88KamCSQ8IutDc0Ea0cnC6RKf7U0e7 WxLoD74HznSlQC+wBp0P5QZSzsBuAM/5PLPXkGRMVV54TZx9/y5Nanh6wmWwH5HH+aEA 0+uPCnysZpMFUjQITWKeehUKXDCi53Lf3UQgVc8OXwa7uiFald/dFmI4WhTdJ6Bdju2z v576xaUmHYg0BmiAr6BVjz4RggT/lbJq9y8F2a6nf1I0GJ3yr5a315j9jCT5W4wr5KMV bPzQ== 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=EIvic+Vew3fa5py89fJxZi5y2z9HPkKVZsFlcgXlCEs=; b=ntuJPj54dIfnw+6Fc+gYPHmRTRW3pHyRTikNEHOcdxGT1L5Ej2PF4R7tHlKOVyf+mL RS1h/2Y6OqeAt/5zXz9NItXgO7b1iuDzL7VkQsB4dYOcxglaVRhSnX9LNIbvyQgmtCUh +SWc+fv2BAfi94eMo4Mh7AFCugwEwuGHLhHnHfxdDmfp6LSq1JWL/9a4HNYRjpknzyaU LlTtG2fGOzy6McUO983s3mnakPJvc2Frj37tvSDl2V8oisN5uLqBrFUKmdQbixWkH0nV UzX9IGzHPKdPb7dfAPuYHEcSFLwHYHT94nkJZSKkF6PtIScJmVTuzjZ1dAuMf+vdb0fv k8eg== 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=EIvic+Vew3fa5py89fJxZi5y2z9HPkKVZsFlcgXlCEs=; b=rlQ2QD9tRcb/CI9dLkcWZCO3wtqGPNufH/+Kpo78lLL0TJPY41eArcly43rfAzd1BU 9SpllX9Xl09r5uOIcAI2TYzJjy4wkKr/k7cdvRmjiEPh4xNr1SNGF7G0F2SvXDedgW5K pop+qw8e+1JVxwT59u/wXk+iMgyfuhUtgaiI/AzcPnaJ1bIcNVx/cSzY1t3RkfP6iRFF QgMBkBjsL85cnj2y8LqqL1q3lRINU7nvXEnisl8GB2aQNlc3bSyNMJWsB3IGRIRpVqGr srtSgy6UMraIkId0aDj9GkudImh/tWBgNFwyWCh8zJ6y1mwUIVrdcJ4ZClJjLhEuUvQk 9wsg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AFqh2koP5nFdGvrwDnHw0HtjrQKc2/EcLjUfZzD49TlCe8Zn+qt7zme/ ktr1pc+cgfQ6YtpaAuhEZ4A= X-Google-Smtp-Source: AMrXdXs6GOVUaErrYnu7D4B9ynEkU0jG7foY4G+iyifZbke/uymeE9uekO4hdRXUcGy4fAlrUWxv3Q== X-Received: by 2002:a63:e554:0:b0:4c2:95ad:fd77 with SMTP id z20-20020a63e554000000b004c295adfd77mr4725627pgj.67.1674992323933; Sun, 29 Jan 2023 03:38:43 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:90a:4fe1:b0:22c:9c93:a12d with SMTP id q88-20020a17090a4fe100b0022c9c93a12dls400234pjh.1.-pod-canary-gmail; Sun, 29 Jan 2023 03:38:42 -0800 (PST) X-Received: by 2002:a05:6a20:baaa:b0:af:89c2:ad01 with SMTP id fb42-20020a056a20baaa00b000af89c2ad01mr45581913pzb.40.1674992322179; Sun, 29 Jan 2023 03:38:42 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1674992322; cv=none; d=google.com; s=arc-20160816; b=05Dw77ZmVUYzYsSQocyiXDP7+8+kvrl4eFxQauetweOSGS+6Im8KaWmyhz2i0SCPo7 L4Utn3tCbYRThxyg70y19vzNagkTHcLNmV9pKLxSfu7lZ7/ofKjQWtlwubkDnwP8ggUI vutlQPta/5ULJoUL/RjZgEdLbBMTEAJo1drnwxsr0tZPY2nvm2BzU1dl8x06kwBXkjM7 CLk/BK8+yY0sVeQLFqSKJRlWp7nbyhV2PDMDIv4K5WNZfoYfo9AVlz2U7hjrBA2Mhrdi mZvLj7iJ4t6pqOxEnRHfEqkLHQfS7fKK0tTMs6ltUhSVs6dr3Acd/IcA8YupLZyHGvil PjYw== 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=KJ9eQwqe1bxNXDo95KUe5pqHwZWI8CL/6triLSo4TBc=; b=LEoq/p3/MMHYH52QcGfHk/sv6WxiXyD5r5OXmGp9xxwU4/MHK9pwRoAMIzOlvcFLOR PvuGC9Y4rpSA6r94dl8Fd0uh0NiwSo94d8yNKz9xkFPsp6NmQpVZKn2a969+cjT2SA9x qz5wtl/t5Dbq0sWYu20sq5RNhiiSyfV5MUe0N2aGJjchfCMod58mJcS229Jri0rhNxsZ ObNFckjIwUL7G3eIlMreiugEtDmt8HJmTdOvZlbeqS15zN7eLL8xKEMWaieG3sj1YsWI kNAUN0C4RGJSSpkOu4ZTdHUUglpSh60UWYs7/OSo5eiJW6569ZQ3pVWiGQizMTiQLUjP H0uw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=HPQR4kbo; spf=pass (google.com: domain of puttamalac@gmail.com designates 2607:f8b0:4864:20::a2e as permitted sender) smtp.mailfrom=puttamalac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vk1-xa2e.google.com (mail-vk1-xa2e.google.com. [2607:f8b0:4864:20::a2e]) by gmr-mx.google.com with ESMTPS id o191-20020a62cdc8000000b0059076272a23si720087pfg.3.2023.01.29.03.38.42 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 29 Jan 2023 03:38:42 -0800 (PST) Received-SPF: pass (google.com: domain of puttamalac@gmail.com designates 2607:f8b0:4864:20::a2e as permitted sender) client-ip=2607:f8b0:4864:20::a2e; Received: by mail-vk1-xa2e.google.com with SMTP id 6so1826040vko.7 for ; Sun, 29 Jan 2023 03:38:42 -0800 (PST) X-Received: by 2002:a1f:9e11:0:b0:3ea:464a:8f61 with SMTP id h17-20020a1f9e11000000b003ea464a8f61mr3912vke.24.1674992321291; Sun, 29 Jan 2023 03:38:41 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: =?UTF-8?B?QW5kcsOhcyBLb3bDoWNz?= Date: Sun, 29 Jan 2023 12:38:30 +0100 Message-ID: Subject: Re: [HoTT] Infinitary type theory To: Jason Gross Cc: Michael Shulman , Nicolai Kraus , "HomotopyTypeTheory@googlegroups.com" Content-Type: multipart/alternative; boundary="0000000000004fecc105f3658aaa" X-Original-Sender: puttamalac@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=HPQR4kbo; spf=pass (google.com: domain of puttamalac@gmail.com designates 2607:f8b0:4864:20::a2e as permitted sender) smtp.mailfrom=puttamalac@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: , --0000000000004fecc105f3658aaa Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 : =E2=84= =9A Product : (=E2=84=95 =E2=86=92 Ty=E1=B5=A2 =CE=93) =E2=86=92 Ty=E1=B5=A2 = =CE=93 lam : ((n : =E2=84=95) =E2=86=92 Tm=E1=B5=A2 =CE=93 (A n)) =E2=86=92 Tm= =E1=B5=A2 =CE=93 (Product A) app : Tm=E1=B5=A2 =CE=93 (Product A) =E2=86=92 (n : =E2=84=95) =E2=86= =92 Tm=E1=B5=A2 =CE=93 (A n) Jason Gross ezt =C3=ADrta (id=C5=91pont: 2023. jan.= 28., Szo, 21:26): > > 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. > > As I understand it, this just rules out universe qualification that is no= t > 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 >> 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 inde= xed >> 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 ("boo= k >> HoTT" wouldn't allow it, you'll have to fix an index), I occasionally fo= und >> it very useful. Without something like this, I don't see how we could ha= ve >> formalised the statement that "Universe Un is not an n-type in a hierarc= hy >> 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-Complicat= edTypes.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 inf= initary >> 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 theor= y? >> >> 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 (consid= er >> 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 ter= ms >> 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=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 h= as >> >>> 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 whic= h >> >>> 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 ter= ms >> >>> 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, sen= d >> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M= 7Yi0i1ChYb8PrP_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/CAKObCaoJMQhY5upSKXT= M%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%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/CAA3CDBYe%2BOnZedPWdVNLKJKfWwM77gVe_-7v4WmU%3DwQd17EkdA%= 40mail.gmail.com. --0000000000004fecc105f3658aaa Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Jason: I agree that externally indexed products imply boun= ded universe polymorphism, but I don't understand how we can derive inc= onsistency from that together with rational levels. The operation that scal= es rational levels can only be defined externally so it doesn't really = affect the possible internal constructions.=C2=A0

To be = clear, by external products I mean e.g. the following for=C2=A0i : =E2=84= =9A

Product : (=E2=84=95 = =E2=86=92 Ty=E1=B5=A2 =CE=93) =E2=86=92 Ty=E1=B5=A2 =CE=93
lam =C2=A0 = =C2=A0 : ((n : =E2=84=95) =E2=86=92 Tm=E1=B5=A2 =CE=93 (A n)) =E2=86=92 Tm= =E1=B5=A2 =CE=93 (Product A)
app =C2=A0 =C2=A0 : Tm=E1=B5=A2 =CE=93 (Pro= duct A) =E2=86=92 (n : =E2=84=95) =E2=86=92 Tm=E1=B5=A2 =CE=93 (A n)=

Jason Gross <jasongro= ss9@gmail.com> ezt =C3=ADrta (id=C5=91pont: 2023. jan. 28., Szo, 21:= 26):
> I don't think access to internal universe quantifications i= s an inherent consequence of infinitary constructors. I'd rather say th= at it's an accidental side effect of Mike's formulation from 2014 t= hat something like "=CE=BB i. Type i" is possible, and it can eas= ily 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 un= iverse.

As I understand it, th= is just rules out universe qualification that is not bounded above by a fix= ed universe, right?=C2=A0 It seems to me that you still get internal quanti= zation over levels less than a fixed level.=C2=A0 And this is enough to mak= e the construction generating inconsistency with Q-indexed universes go thr= ough.

On Sat, Jan 28, 2023, 12:46 Michael Shulman <shulman@sandiego.edu> wrot= e:
Also, apparen= tly 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 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/CAKOb= CaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.com.<= br>

--
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/CAA3CDBYe%2BOnZedPWdVNLKJKfWw= M77gVe_-7v4WmU%3DwQd17EkdA%40mail.gmail.com.
--0000000000004fecc105f3658aaa--