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 18734 invoked from network); 31 Jan 2023 01:12:16 -0000 Received: from mail-oo1-xc3b.google.com (2607:f8b0:4864:20::c3b) by inbox.vuxu.org with ESMTPUTF8; 31 Jan 2023 01:12:16 -0000 Received: by mail-oo1-xc3b.google.com with SMTP id h1-20020a4abb81000000b005178afbdbfcsf532937oop.11 for ; Mon, 30 Jan 2023 17:12:16 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1675127534; cv=pass; d=google.com; s=arc-20160816; b=DrTsqGB+232fIxP5MMJCclXzHjOmHv4rFJqSLXjqrzodFi3hgnuCY1K1Km4Vt2NkG1 QOVE9wuF97i79mHLvFZ9wl9N7iUSRqsGY6tyzmhFE/hGwaIF17jzbf6hXU/w0VQuIQUt Yqf/Cn9DHA21F4sBxK6wuqA3E+YgBezCALMhS0G7oErJ6zXd58xbd1QMuycp2J5KXF9Q EfZ1ZZac7WieMGZc8+t+x954wu1tVIAjU7bEtAMXS2pUsGPQLcGqaOWRP5UXTRzxW/3u MBF4xRBfhS9LPVG5qedNTJ6HvK1nN96w9RxoLIRGj7MPknNMXxk9KXOucVYrKq8sHZ7l cwig== 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=fui+iBIMbl222bYZIi2b+7ljgv8voiOOqDUqS8t6xUw=; b=lqsVt9WB0A1gLB78EZRZeSM0mVLd7lfXevQA66otAa3O0EiNwRCkvB/B28jp/B/BGb GQyE1jvyu6SujwRsP4I/nXHmeWMjCZMnHta9KS7W8RekKZITGwh9z0cWx5hFwiJg+soE 6ergZaPaA+BNs+K2+sPs0++QCzr5o8hnMFaXXpmIyQMyd9Ralj5AYmgyaFx1dIgOU2by jjWlxtT4F8mtJnJN3Fw//hvXQItvNfCuvtFQYXAnqurqDcbLEGqyau4u4tzx4aKQmph6 f5qJOufyk4fDFGkv6eN+sLbAnSk8JcJ3RMIf2y2BehTXX36ynlIKH0lj52YiG46IU3p9 En2A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=UW0Q9o8R; spf=pass (google.com: domain of jasongross9@gmail.com designates 2001:4860:4864:20::2f 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=fui+iBIMbl222bYZIi2b+7ljgv8voiOOqDUqS8t6xUw=; b=ej03zy9YKBkNj7FBFcyxP5BukLkRMlrdXOYLxpW9qH45yS/W9xGYp7SpmdCOJFEyZh W2o/V6SXZO9v9qxKE4rBHqQND3HoxWCJZ7BOBdRaRwL8o+S9GDGhPsYWwCzY++cn6YV4 XmykZDmSDPsmwZnOet87r4XEQ0a62+lqROMuWq0Y/GA6D1k8dEbPR6p6joukMZ1MYGM9 E1w1T1VoVeSZlo/F5u0X7P4Kqo9igthjgsnNVMvIc8pr6s7WUErWGTdXlvzDzqOIjqLH ZLN9mgFXmqtiz2QrEiOSzQ7b34GwZZEPSyqYy7NVBmePKJDPBgxOS9maPuw6L09Md8Ru WXuA== 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=fui+iBIMbl222bYZIi2b+7ljgv8voiOOqDUqS8t6xUw=; b=WL0TQhq+BJ7Dne3RmDeXCSYNFCHV7TYXhfzB/W8aWCNOb6+OJNgOkizUpBwKf5wIMa GHnitjzVnqV9R3VCPppSlWsHakUfgdsQi5rqLWWfxwyH4wVWuAO7l2y2Q14uVIPSk1+m 8aUInIIl0k51Kbdk+MxhCzLSG+y985oMkG9YY+txoYeL3nyQduEjgTe7cPJAIBvf13F0 iTmTxpwyEEJk1aYIjA6VOh74ab79HGVvPiy+hPq7RuvDd/QykjMCRuxdiOhCMD+ZiPko r+KZoiCMgo7LcXQKwQUhFH33NQ8zMCymdwCm3o5U9sfU/2cDHWWhXe9stE3iX1eKVMQ9 qlFg== 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=fui+iBIMbl222bYZIi2b+7ljgv8voiOOqDUqS8t6xUw=; b=3h7KVbrwjfAipADTr+Zn0xXicWJK3VQzMBTSy4OHRwLGkJRJXvjrwCw1NmScbGtOKp 8TTcr+JW1Sn8lAyPOxN1mclZN8sXP7UTTeetzsI40hLOlxA3L1v4FN+To2ikw6TsA9PT ZZoF4nR74rsAf9uu8j307rdDxFrfQyQtYbd/irqiSoReeXF2pBfXV8dZ8I/WrZkTZI6j 2IuefDrIYdbRa1WL9jOoHmXwxJDY3CoaRfK5CawoCpClErXbMXxm5GaBT+eddmfWRnks 1CY2Nq545EPaSvbsIzKAZze/ZYqS5HAaxv77ENH8hKHmJgbXZQ6XfIj5UitcDfFDhGEy eGqA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AO0yUKWQkHo0pNlyQY/R9v159oAcmoyIa3fm/I7wS4bJ8u6c+WSan3Nm HGLQuL7IZRwnnM6wH8bPilQ= X-Google-Smtp-Source: AK7set9CTYQPXpa2zcCDraBmz/MULZ/xZR3JMqFIT/v87BZVf65MdHqavdEdeYYYZhc+lkZz749UOg== X-Received: by 2002:a05:6871:8a4:b0:163:bd1f:9e21 with SMTP id r36-20020a05687108a400b00163bd1f9e21mr517906oaq.200.1675127534615; Mon, 30 Jan 2023 17:12:14 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6830:6301:b0:661:b84b:eb5e with SMTP id cg1-20020a056830630100b00661b84beb5els1998306otb.3.-pod-prod-gmail; Mon, 30 Jan 2023 17:12:13 -0800 (PST) X-Received: by 2002:a9d:7614:0:b0:68b:ca10:4ad with SMTP id k20-20020a9d7614000000b0068bca1004admr3831220otl.31.1675127533478; Mon, 30 Jan 2023 17:12:13 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1675127533; cv=none; d=google.com; s=arc-20160816; b=OQAsvfs3mqQqGqK1XqbuKdFLFbejV+M0NXjvuEBJDUY+EAkDbk99B/DDVEGHdRlx7z SRVlPqdFs3vwV4jiiIISAPSYcKOfH1xgRNdnt5lz4YytTuF3GDQyUAp8X80Qz2/UvZRX kvbGx6jVYey1VjfGJivvKw5A7PT9yfVi8w3FA/J5RfjUHtIz5ppxWA+PIcv07ANObz/d Lt+d7iW1O27Fyz95FnUdc/++/1XHijY6HYkey/On6vD2wAvi88rnGLlkVOgTk95ET5Ms OAGcvP4zObhoVPozi6DBCDa/D1pClSiyO3FLWRQRUhxvFPK0wxHNLwduwIFvYVyHwXVb J8Dg== 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=WjWsZETbMFzjKzg6i4Tjl9v0gfxc/hqreg82YFsPi60=; b=cH62Mo0Pj2ElkRSO4aY9R72RsmfClx0ENnqu7iyQot2hkk0d1jECInCxpMu/O7F0YD ULWyPje/5Eqdrm/qfuiPDTHGj/6RBerahLevzhpnhhd0Hjr2wJhCFAlD04selqV+IQfM 1dJH6Q5E7i4H/JNZ5GQ0WygLfr2m/OugUuk+qaIkyefrVj5ReOk2JaIFWxyvMePgQcKP k4BVYxKNmWDrB5KYm6otM0fIFVF0kDO1xDzZtA9aUrqaPBH7ENdVOqPBDygQL2WKh5Ke UUUcTIUdxX3BE8E5XNAopEA+/T+k56ODK6fOhl6GLpjKTQfCNzsFV5CAC4Iy2Sch1FRk xGog== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=UW0Q9o8R; spf=pass (google.com: domain of jasongross9@gmail.com designates 2001:4860:4864:20::2f as permitted sender) smtp.mailfrom=jasongross9@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-oa1-x2f.google.com (mail-oa1-x2f.google.com. [2001:4860:4864:20::2f]) by gmr-mx.google.com with ESMTPS id br28-20020a056830391c00b00686566f6f48si1675117otb.0.2023.01.30.17.12.13 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 30 Jan 2023 17:12:13 -0800 (PST) Received-SPF: pass (google.com: domain of jasongross9@gmail.com designates 2001:4860:4864:20::2f as permitted sender) client-ip=2001:4860:4864:20::2f; Received: by mail-oa1-x2f.google.com with SMTP id 586e51a60fabf-142b72a728fso17504018fac.9 for ; Mon, 30 Jan 2023 17:12:13 -0800 (PST) X-Received: by 2002:a05:6870:5688:b0:163:2d66:de03 with SMTP id p8-20020a056870568800b001632d66de03mr1676951oao.34.1675127532987; Mon, 30 Jan 2023 17:12:12 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Jason Gross Date: Mon, 30 Jan 2023 20:11:45 -0500 Message-ID: Subject: Re: [HoTT] Infinitary type theory To: =?UTF-8?B?QW5kcsOhcyBLb3bDoWNz?= Cc: Michael Shulman , Nicolai Kraus , "HomotopyTypeTheory@googlegroups.com" Content-Type: multipart/alternative; boundary="0000000000008eab8305f3850595" 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=UW0Q9o8R; spf=pass (google.com: domain of jasongross9@gmail.com designates 2001:4860:4864:20::2f 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: , --0000000000008eab8305f3850595 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Ah, you're right, sorry. I was confusing "being able to name particular universes as function outputs" with "bounded universe polymorphism". I retract my claim. Best, Jason On Sun, Jan 29, 2023 at 6:38 AM Andr=C3=A1s Kov=C3=A1cs wrote: > 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. ja= n. 28., > Szo, 21:26): > >> > 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. >> >> 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. An= d >> 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 somethin= g >>> 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 ind= exed >>> 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 ("bo= ok >>> HoTT" wouldn't allow it, you'll have to fix an index), I occasionally f= ound >>> it very useful. Without something like this, I don't see how we could h= ave >>> formalised the statement that "Universe Un is not an n-type in a hierar= chy >>> 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 considere= d >>> 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-Complica= tedTypes.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 in= finitary >>> 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 (consi= der >>> the function `=CE=BB i. "Type"=E1=B5=A2`). I believe HOAS-like interna= l-level >>> quantification rules out any "fractal-like" scheme of universes (such a= s >>> 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 te= rms >>> 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 >>> 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. Wh= y >>> >>> can't we have an infinitary type theory? >>> >>> >>> >>> An infinitary type theory would include type-forming operations whi= ch >>> >>> 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 o= f >>> >>> 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 appropriat= e >>> >>> externally-defined tower of fibrations. >>> >>> >>> >>> Has anyone studied infinitary type theories before? Of course, the= y >>> >>> 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 ar= e >>> >>> 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/CAKObCarzP9wE1t2Y8= M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com >>> . >>> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaoJMQhY5upSKX= TM%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/CAKObCaoZUnvTfEOPdX8nwOUZM_M%3DnEoszZYizE4%2BypoymDLozQ%= 40mail.gmail.com. --0000000000008eab8305f3850595 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Ah, you're right, sorry.=C2=A0 I was confusing &q= uot;being able to name particular universes as function outputs" with = "bounded universe polymorphism".=C2=A0 I retract my claim.

Best,
Jason


On Sun, Jan 29, 2023 at 6:38 AM Andr=C3=A1s Kov=C3=A1cs <puttamalac@gmail.com> wrote:
=
Ja= son: I agree that externally indexed products imply bounded universe polymo= rphism, but I don't understand how we can derive inconsistency from tha= t 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.=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 (Prod= uct A)
app =C2=A0 =C2=A0 : 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 = <jasongross9@= gmail.com> ezt =C3=ADrta (id=C5=91pont: 2023. jan. 28., Szo, 21:26):=
> I don't think access to internal universe quantifications is an= inherent consequence of infinitary constructors. I'd rather say that i= t'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 t= ype theory with such infinitary type constructors is specified without allo= wing internal universe quantification. This is essentially because the exte= rnally indexed sequence of types still has to live in a single fixed univer= se.

As I understand it, this j= ust rules out universe qualification that is not bounded above by a fixed u= niverse, right?=C2=A0 It seems to me that you still get internal quantizati= on over levels less than a fixed level.=C2=A0 And this is enough to make th= e 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 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/CAKObCaoZUnvTfEOPdX8nwOUZM_M%= 3DnEoszZYizE4%2BypoymDLozQ%40mail.gmail.com.
--0000000000008eab8305f3850595--