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 29980 invoked from network); 27 Jan 2023 20:41:10 -0000 Received: from mail-qk1-x738.google.com (2607:f8b0:4864:20::738) by inbox.vuxu.org with ESMTPUTF8; 27 Jan 2023 20:41:10 -0000 Received: by mail-qk1-x738.google.com with SMTP id bm30-20020a05620a199e00b007090f3c5ec0sf3693007qkb.21 for ; Fri, 27 Jan 2023 12:41:10 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1674852068; cv=pass; d=google.com; s=arc-20160816; b=raaEZRZg5YAVyy0/vee2VNwGRXtIjGxenvOE+3SbH5GKT6DO9bKlCACIxAt8mQZdex 4OBRhaNRkWb2OcBVkvIaBrAaun9eMCMYj5Lhkz7kmsZ/DybIxBadZf6BRUXR2SlyqAWT hCjISfyeX38yRJc8Eqf+uf5E1+37UnsndGtCNru2cHPLOqFWMF7aXmmmIvk8E4xXywbF 763+zSH0+cUYlk2kA8NMhZao3cbYDlL5fUEvvR70HO7sJrplBMyLTm/3vhR8LPaoc+K3 BiZwEb+QcayRAVT8n+H7ZSj/qkyvcWSnpO0NY71sRfHGzb1vEDshBTNu8hL6qUhEHELS 3w6A== 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=X2DANt7h0JRyV6NRyTMrMi/4Wp+fqGHMmF5YdNapm2Q=; b=dCtUNQfnq8wjq+GKu3rLGGMm157ypBLQIVZMXaFbyhYPnzmQ3qiK7z6eKDYgHNlBSE b7mGBeUNAwwza2zCYQUvSPXaa3Os5mSm0uxWzBeMZACY9S24RmY6A4/pjftPtCra0uDR bzPcdltDgnTKhfgM+J3GAvwIKwY68Dgy685uhJqYsdQuMf9O/FUOACeEWIS+hAT3mID7 SUB/RHeY/9aUqL3lnSAvwc4WE0odlPW1biDEHLxepkv4Wn4Ds0aLyTbFpEHy/CXLSxei E1t0nOwL71Wrp2+MScYIYA1Fik5RdV4ndc00lLqRiAsCeOjHnm7p8BZg3eBRcJk+grf0 VakA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b="lG/w6DwO"; spf=pass (google.com: domain of jasongross9@gmail.com designates 2607:f8b0:4864:20::330 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=X2DANt7h0JRyV6NRyTMrMi/4Wp+fqGHMmF5YdNapm2Q=; b=XThF1+sPeqUUdWLTxQJNQN6JSPr67sc1a17zyk/hE8gEIfrHdqs8l2zMfMgNPpd0nS c2xojbtgg71bbdpcdRZUDBxvo67E9qpUwKXyJm1j3enTZFE/QJNQ/SCv+5DJEfjLb5IT AqcIIL/fD+i0FoDX5U0nPoYbZK+qwjkqwez4KNEiPD0BMtJmFSQL26ofpzFiaC4/P5yw wPkPoURnohMNIjkINdSRwicWrVG3i1EVeT2Jv2kQ8A1HSf700+A0PA7VohFocb0qsl87 su807pz12BPWXDmca164DIhxxnt7xW26PQwUCEXOHmZQmQLHHcOorLEGdH3ogEu181nO ICDA== 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=X2DANt7h0JRyV6NRyTMrMi/4Wp+fqGHMmF5YdNapm2Q=; b=Puqh0MUD6UBYeSbRFPtwoIZEGrv/1usB3RGRYgbnM6NXjNIWl+3ttxk9cHQaYK0+yE Ssr3H8aqVxzoSWVlTcI4mg4InB3AQLlJ8xsaQiK7NH8n339zLscJQEWYmJhY4VcRZgoW 5FCySph8bWM+sS08Ua8z29+UQ+l/KcfQB3zh4i4FqA0UgE08c4Gkki5Q17EPbh7Vl9h1 8xlGLYP0mROIif8JvQ+37xED1OY5aFbblK631dp3R2+++fkqj6sHkKof7br7QF7ZqsL8 gcxoe22S4Ay2v4DtPQ095QKdBwGLsPGzsWPmmnPJ5Hy0O/XTgLuOvYsQDRFjHNgdd0xs 0QzQ== 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=X2DANt7h0JRyV6NRyTMrMi/4Wp+fqGHMmF5YdNapm2Q=; b=hpTSzK12x6Zwxe5HEM3Rtb1UrPy3iIdzzDfsHO7ZL6jHFWH40BTagOD8Vdu9xgObq1 SgkLENO54FXhyvlgOKxdIm1DTOZ8KxBzFCvMUh7C5U/1MDT8pyDyokbwIToWjMjnHoiK XPSiUKBle1/wTeT0rfZyPiZDknoSYeuuH28uWcZq1T8vkG7wq4OzDS8PC4Iqeb4u28uK L9YS09yqI/d7BKXD5a9F6Ifoj/YxaDWKhH0ApnZmaPHk1Z2NSaft2WnWTP22eJwOSF2z Wpnmy0kqwfxCLqsW5u1Jp5gNx+7136bR4W6Zm+ns2glqa3A4CP5czPFLYE5aEARK63/O OZtA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AFqh2kqApQeQ3eY1NWw+oXMH/xHAr2cuKcN0aE3hSU4GHcetQxVjECMe WOAUUlcTSK5m6fINkXARdPE= X-Google-Smtp-Source: AMrXdXt3vIOw8O+RnWzSchoQ7ejbkjzWvQAkwHkVjaQcI3qFT8dm+x2ZLPzz3PIBI1ycKMXYSM8uSg== X-Received: by 2002:a05:622a:1dc4:b0:3b6:399f:ab85 with SMTP id bn4-20020a05622a1dc400b003b6399fab85mr2160563qtb.286.1674852068034; Fri, 27 Jan 2023 12:41:08 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:71c4:0:b0:3ac:c6f0:fe49 with SMTP id i4-20020ac871c4000000b003acc6f0fe49ls4559287qtp.7.-pod-prod-gmail; Fri, 27 Jan 2023 12:41:06 -0800 (PST) X-Received: by 2002:a05:622a:1181:b0:3b8:2e36:9d24 with SMTP id m1-20020a05622a118100b003b82e369d24mr2987167qtk.50.1674852066576; Fri, 27 Jan 2023 12:41:06 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1674852066; cv=none; d=google.com; s=arc-20160816; b=SIUn+9npYfAC2Z00b2HQjElgBI3rFwSuoja30udmE2baUiEGywx9bYD3EIcdcbhWhW LcLSgnRUDwhL6ujKzVLf9HXE6insSaTW+oSLlsRGpQoyqAH9ODlYmC/+fEuhT/iZC6hb tVhKfHncaXrTRZaUpeYlrx7gUWFKb6REEG5OATx8vBhCycJEC1YO5yxNuBgzEgu0nu03 p3G1KXKHQ5vj4UHP2czS89ceY6S5xcCJI1c5MiJZwdUBqpJ2Gh0HVc1w4gQXRJaXvsj8 BM3Ak6GuKMsEmPneLi5FmP9bOx1SbUGiZqpX8Urd4vtIoZqPY+m0Hkzt9A3EgfVjAHLR eiPA== 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=Ue00dToyzlruRbxNqHoOFzXrdr7vtyDj6qoMZWpgm/c=; b=T4kS/pOpFDtKONysidhTuEtkGwEhAo08PbeB8cn+r0RtiW+jmZ1Fm4i63urX1+ZEkA EyY+MDU9TPdQwN9T53LVzF/E3cHJD006xHtNfF5oNPgDZsI4SOE96GazKMfXSmkCF1vM EDCc+bGk1Q6/Da1TV4pgFPhJ2LMWktdqKkbGO8HzPjQKZfV6xwAZGpffLqucIj++r8qS FR50AKEvNJtzblnr1jpBG+R8rK3vzOESCP8XflT/AqX9Joe7Q2bH1hLHIQUsqIihXt9Y Tuf2NzXtk8zp31DILUhb3K+kveSR+ApDJdVBzjwoeXGpP/MiOGhOJwczhd+HC6MYoEy0 mBiQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b="lG/w6DwO"; spf=pass (google.com: domain of jasongross9@gmail.com designates 2607:f8b0:4864:20::330 as permitted sender) smtp.mailfrom=jasongross9@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ot1-x330.google.com (mail-ot1-x330.google.com. [2607:f8b0:4864:20::330]) by gmr-mx.google.com with ESMTPS id bi4-20020a05620a318400b00705bf2df50bsi372243qkb.0.2023.01.27.12.41.06 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 27 Jan 2023 12:41:06 -0800 (PST) Received-SPF: pass (google.com: domain of jasongross9@gmail.com designates 2607:f8b0:4864:20::330 as permitted sender) client-ip=2607:f8b0:4864:20::330; Received: by mail-ot1-x330.google.com with SMTP id g21-20020a9d6495000000b0068bb336141dso709779otl.11 for ; Fri, 27 Jan 2023 12:41:06 -0800 (PST) X-Received: by 2002:a05:6830:600a:b0:684:cec7:aeff with SMTP id bx10-20020a056830600a00b00684cec7aeffmr2167764otb.70.1674852065976; Fri, 27 Jan 2023 12:41:05 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Jason Gross Date: Fri, 27 Jan 2023 15:40:42 -0500 Message-ID: Subject: Re: [HoTT] Infinitary type theory To: Michael Shulman Cc: "HomotopyTypeTheory@googlegroups.com" Content-Type: multipart/alternative; boundary="00000000000071a82205f344e2b9" 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="lG/w6DwO"; spf=pass (google.com: domain of jasongross9@gmail.com designates 2607:f8b0:4864:20::330 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: , --00000000000071a82205f344e2b9 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable (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 infinitar= y 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 (consider 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 terms with universes between 0 and 2 back into terms with universes between 0 and 1 (divide universe indices by 2), and this loop gives inconsistency by G=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. Why > can't we have an infinitary type theory? > > An infinitary type theory would include type-forming operations which > take infinitely many inputs ("infinite" in the sense of the > metatheory). The most obvious would be, say, the cartesian product of > infinitely many types, e.g. given types A0, A1, A2, ... (with the > indexing being by external natural numbers), we would have a type > Prod_i(Ai), and so on. Semantically, this would correspond to a > category having infinite products. > > More useful than this would be a category having limits of towers of > fibrations. I think this can be represented as a type former in an > infinitary type theory as well, with a rule like > > Gamma |- A0 : Type > Gamma, a0:A0 |- A1(a0) : Type > Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type > Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type > ... > ---------------------------------------- > Gamma |- lim_i A_i : Type > > Then we would have a corresponding introduction form, like > > Gamma |- x0 : A0 > Gamma |- x1 : A1(x0) > Gamma |- x2 : A1(x0,x1) > ... > ------------------------------------- > Gamma |- lam_i xi : lim_i A_i > > with elimination and computation rules. We might also need an > "infinitary extensionality" axiom. > > It seems that in such a type theory, we ought to have no trouble > defining (say) semisimplicial types, as the limit of the appropriate > externally-defined tower of fibrations. > > Has anyone studied infinitary type theories before? Of course, they > probably won't have all the good properties of finitary ones. For > instance, I think judgmental equality isn't going to be decidable, > since there's no way to algorithmically test the infinitely many terms > that go into a lam_i for equality. But other proposals like HTS are > also giving up decidability. Are there other more serious problems > with an infinitary type theory? > > Mike > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --=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/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40ma= il.gmail.com. --00000000000071a82205f344e2b9 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
(Resurrecting this thread because I stumbled upon it = while rereading A Formalized Interpreter, and I believe I have som= ething new to add.)

As I understand it, using `=E2= =96=A1A` to mean "syntax for A", an infinitary type theory has ru= les 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 semisimpl= icial types coherence issues.)

> Are there othe= r more serious problems with an infinitary type theory?
I think t= he answer to this is "it depends".=C2=A0 In "An Order-Theoretic Analysis of Universe Po= lymorphism", Favonia, Carlo Angiuli, and Reed Mullanix have a cons= istency proof for a system with rational-indexed universes (and no explicit= universe level quantification).=C2=A0 However, infinitary rules give acces= s to internal universe quantification (consider the function `=CE=BB i. &qu= ot;Type"=E1=B5=A2`).=C2=A0 I believe HOAS-like internal-level quantifi= cation rules out any "fractal-like" scheme of universes (such as = the rationals), because we can write an interpreter for "terms using u= niverses i with 0 <=3D i <=3D 1" into terms that use universes b= etween 0 and 2 (because we have enough universes to do that), and then we c= an embed terms with universes between 0 and 2 back into terms with universe= s between 0 and 1 (divide universe indices by 2), and this loop gives incon= sistency 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.

Be= st,
Jason


On Sun, Jun 22, 2014 at 2:05= AM Michael Shulman <shulman@san= diego.edu> wrote:
Since the problem of defining infinite structures has come up in=
another thread, it may be a good time to bring up this idea, which has
been kicking around in my head for a while.=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 operations which
take infinitely many inputs ("infinite" in the sense of the
metatheory).=C2=A0 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.=C2=A0 Semantically, this would correspond to a
category having infinite products.

More useful than this would be a category having limits of towers of
fibrations.=C2=A0 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.=C2=A0 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?=C2=A0 Of course, they probably won't have all the good properties of finitary ones.=C2=A0 For=
instance, I think judgmental equality isn't going to be decidable,
since there's no way to algorithmically test the infinitely many terms<= br> that go into a lam_i for equality.=C2=A0 But other proposals like HTS are also giving up decidability.=C2=A0 Are there other more serious problems with an infinitary type theory?

Mike

--
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. For more options, visit https://groups.google.com/d/optout.

--
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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP= _2RpKY9tcEZbkB9QKQ%40mail.gmail.com.
--00000000000071a82205f344e2b9--