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.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 27405 invoked from network); 28 Jan 2023 17:46:06 -0000 Received: from mail-io1-xd3a.google.com (2607:f8b0:4864:20::d3a) by inbox.vuxu.org with ESMTPUTF8; 28 Jan 2023 17:46:06 -0000 Received: by mail-io1-xd3a.google.com with SMTP id c13-20020a5e8f0d000000b00712d1a91eecsf2239260iok.5 for ; Sat, 28 Jan 2023 09:46:06 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1674927964; cv=pass; d=google.com; s=arc-20160816; b=zfbsQC3e1Axbezdxytgzaah1fzsJYF2hKjh2cG84glaNhYOn7tCBgLu4z9RUfl+29G UoQwx6zOdntvmpN+g1EHszzCH0Ac0gt1i67wdzg+P4cwq9yVYNpK9QcZTjd6VsKx7veX HQizX2ytai90BmpkhgFpMpuYVteiZwvOFm0Ioeg3FOrLMChCZPXJRjR057Eli4xSud7r UQYMapYa9oKyI9pcn51bQs4O8ovPlY846n15as28B1knPzkaE2kR9n8cLde978qEAZc8 7McRo1zs8zs4mMo2z0eEfE7wfBvhdjQdHepe+tQK+qhsXmBlZaVopVUIRMq2Ip/uwTxF yWpQ== 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:content-transfer-encoding:cc:to :subject:message-id:date:from:in-reply-to:references:mime-version :sender:dkim-signature; bh=uG6q6eKC4MOdlXS2HrbpLiVv2E3gabP00G3m+sn1cLw=; b=GhJZLh8yysF1B95gZITRLjHU9cxnoeF+CdE73bFKjjGRZ2+zwuCws9swHQWmzIGs8D oBVy35KJQZVS4lsEa/ReKW/4ErJd9J4b5GlaRv0bvDaBqzg0+Mk8ggT0uufuLV81CYSM kmaL0el08yElN13NRep9bf3k5aKEjZIw3ExL0wdTQf2xc+DTNb8kffx5vcJ9J9G0GY2q qavbCIWH9iy5xeD5fKJ8RomVTylIBWHLWbIJ9Q89ClVRgxqEusxsdiwGhxvOSFAXCD/t paU2yHdb/dIdu4vWM6FZtVM92d3DOTI2BGQA8Wb7q41V0/PPMbRT+T1Mb1ncAOlo3QEP 98KA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=SZd1Yh97; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b33 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu 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:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :from:to:cc:subject:date:message-id:reply-to; bh=uG6q6eKC4MOdlXS2HrbpLiVv2E3gabP00G3m+sn1cLw=; b=HsWc94KvwdmiCn36p8raAnVXrjOrDCEBFbqPUxR2eV8BppyzQyxlEzlTP/OAp+4Vri RSwukDLpCUXybzeab5piC50V5myBy5KKUtIofqbTfP6spc0Zkeiw1XEYKzVqcORpe3xT 6Hl5sIee57sMw+t3KuV2pwMLZjN50Ql2J9Re6cpl5LgUzetJIfBDecsSV3QUA6VxmM0f HJRfNg6Fn5KPebgWl6L4eOhuF0IxWNVy2087QoUrnYoNjK97fEEg2tGJ+1i9Nt7kN0hw dc0eJnWr0Ci0v6lxj6umpgg01B5/bhJV7pXZS+D9zGjOBkSZyYlJNzrRD0LKizHviGdI CzKQ== 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 :content-transfer-encoding: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=uG6q6eKC4MOdlXS2HrbpLiVv2E3gabP00G3m+sn1cLw=; b=jWr5TYsqwd/cw1ACsDMWyuMvD0FVy9oNNRdUmrLlwQqp3C1TwnmOXkfHlhAdUE3ETM MMO55hG3CtLAclNmpIBYUOwYAZDcn1lwo1nDmKmqUu3nDn9IvdWhkG6YScPEz6/vu2Bl oIukiherVUbIpiwcg5ghxVHx65InTC1FkVtlgkPFR3ZqJz9g8GwIbkMyOr1J7QeAj6RH NR6wLmP49+y01wU3LT8tIOq3S75RWA831MPiSkmVWmeT7ILtsxEE3ew85gwL8j7v9vo4 6lpajTFeuX8rbLrMqVSpzHaq/yg13Hqk94UP9Gu55wU9JUpMqY39LbGx++YudKUtOV/Z rdbg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AFqh2kqlGtpy7t7gXZJFn1m4UM/TAscdqsNM49Ij/QDmM5s1S94mQgWW h0Zcc9Ba5Hc44JpQyGXYH8M= X-Google-Smtp-Source: AMrXdXv3lVv0/BzT0ttTj7qB401igG8lyVX3DzBxAZmWo1Qin96WPftI4/lAFKMwXWYZ+0XLhZQFsg== X-Received: by 2002:a6b:510b:0:b0:6bf:e923:388b with SMTP id f11-20020a6b510b000000b006bfe923388bmr4559881iob.105.1674927964509; Sat, 28 Jan 2023 09:46:04 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6e02:348e:b0:30c:27a9:a355 with SMTP id bp14-20020a056e02348e00b0030c27a9a355ls2853480ilb.3.-pod-prod-gmail; Sat, 28 Jan 2023 09:46:03 -0800 (PST) X-Received: by 2002:a05:6e02:1c25:b0:310:a5a4:73d6 with SMTP id m5-20020a056e021c2500b00310a5a473d6mr12232925ilh.9.1674927963257; Sat, 28 Jan 2023 09:46:03 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1674927963; cv=none; d=google.com; s=arc-20160816; b=tSiMv8ckVjepSiOcbIkjjd4a+IQ3vLgiO07NRkYjlXrUrS0WwO/NlLd8mg8rJj15un xjdyz20PjJwRgfdFTXSMSuEc0glQ8QLqOul+psX+g8lpDc2dLhp8in5aGMZF1lB/6BSr eymZmlLyltBAIhK52vNBCFwRSuHJtGJiqYJmwB2rRXN3zvKmHTGLDuvbCT2fcOMxzeBx EqW+Tut9y36c0vKANHhWRREhQAMbILXjJVJfkZBEJOX/QGs+Mg09Ao658VxwDgwL5NJc fipceWfPUFbEzafdRCqnyuDlmaOfUQ5kstwHg2jr/tPgF/I0kcI8mH8bRjNa0LwIINuZ 4meA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=8XsU7xo5io/FgtBSfji0AfEqj1BZh+V2AxEvd5gp2lU=; b=n3Ds8hq2p0fjjkRI1NyU10xEMLbkjY/2kQOubffIL1kvjYgYtVno3Azn4IEDzkZeDm AtrUOBU+IjjQ9SWWbuVVJteTYiS07JyqfMXNlJbixfVNz+7b8N1RpLnO3zeklBWhPC6v Y/HiivvE6K4IMNQE6aJ4b0/lTyFIFckL+PbvjOswHuLZ5wrlR5R9Ac3nI91IDUInq+Gx YVx/svbk9ng8Xc1qLLr1Cr1/lgtWub8bR6/TlRE6QC86UCmbkMZ8heZpDrFHte1twip0 BlYuKuXYnpzAhaSWTQ4v9ec0g5+bvYtbyDA90RPqzxT5+M9pRtWyXsSMya+fbFZyY4Rd 3feQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=SZd1Yh97; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b33 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-yb1-xb33.google.com (mail-yb1-xb33.google.com. [2607:f8b0:4864:20::b33]) by gmr-mx.google.com with ESMTPS id v11-20020a92c80b000000b0030d87b97b25si593156iln.4.2023.01.28.09.46.03 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 28 Jan 2023 09:46:03 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b33 as permitted sender) client-ip=2607:f8b0:4864:20::b33; Received: by mail-yb1-xb33.google.com with SMTP id a9so9611569ybb.3 for ; Sat, 28 Jan 2023 09:46:03 -0800 (PST) X-Received: by 2002:a5b:604:0:b0:80b:65cd:c6dc with SMTP id d4-20020a5b0604000000b0080b65cdc6dcmr2496879ybq.138.1674927962863; Sat, 28 Jan 2023 09:46:02 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Sat, 28 Jan 2023 09:45:50 -0800 Message-ID: Subject: Re: [HoTT] Infinitary type theory To: Nicolai Kraus Cc: Jason Gross , "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=SZd1Yh97; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b33 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu 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: , 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 wro= te: > > That's an interesting observation! However, I think the question of unive= rse hierarchies is orthogonal to the question of infinitary type constructo= rs. > > I don't think access to internal universe quantifications is an inherent = consequence of infinitary constructors. I'd rather say that it's an acciden= tal 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, st= rengthening A1-3 of the 2LTT paper [1], a type theory with such infinitary = type constructors is specified without allowing internal universe quantific= ation. This is essentially because the externally 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 vie= w 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 foun= d 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 externa= lly indexed family of Nat-many proofs, and it's only a lucky accident (usin= g a feature of Agda that isn't even part of the considered type theory) tha= t 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-Compli= catedTypes.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 F= ormalized Interpreter, and I believe I have something new to add.) >> >> As I understand it, using `=E2=96=A1A` to mean "syntax for A", an infini= tary 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 expl= ains 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 Anal= ysis of Universe Polymorphism", Favonia, Carlo Angiuli, and Reed Mullanix h= ave a consistency proof for a system with rational-indexed universes (and n= o explicit universe level quantification). However, infinitary rules give = access to internal universe quantification (consider the function `=CE=BB i= . "Type"=E1=B5=A2`). I believe HOAS-like internal-level quantification rul= es out any "fractal-like" scheme of universes (such as the rationals), beca= use 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 enou= gh universes to do that), and then we can embed terms with universes betwee= n 0 and 2 back into terms with universes between 0 and 1 (divide universe i= ndices 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 mor= e exotic universe level structures. >> >> Best, >> Jason >> >> >> On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman w= rote: >>> >>> 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 Grou= ps "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 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/msg= id/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%4= 0mail.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/CADYavpypv0OieLCmivNYHYf7f8VnN1zWaKbafO-EP7kkPxg1dA%40ma= il.gmail.com.