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 9467 invoked from network); 28 Jan 2023 15:21:25 -0000 Received: from mail-ed1-x53c.google.com (2a00:1450:4864:20::53c) by inbox.vuxu.org with ESMTPUTF8; 28 Jan 2023 15:21:25 -0000 Received: by mail-ed1-x53c.google.com with SMTP id y2-20020a056402440200b0049e4d71f5dcsf5433842eda.5 for ; Sat, 28 Jan 2023 07:21:25 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1674919284; cv=pass; d=google.com; s=arc-20160816; b=Qt0vA513pn+/2BMXmvcVMDC8KiO7h6g+P5ZIzaPcKjwOCgLtDIn7ys0wpFhidD6mBf xd5hmQlG+H6hM6h5p4jwrQr70hgASlkeqL5pQIE7nnKd8TtgFQELfUclZxzQ3KnQObB9 1oiw7ZNXoiosI3jZjRxwcWMHJanLxstOagdDQqpWzR2v9x3B3kvuPPlOXAwOzZdZoUWY 84X+iSu6XwC1yGMA9mk8EoN9cYVo7WgwoklwRNCPIAJ0uNwy9Vlu6bf3pRdd90AZIuGx EyqHsUb5ZHA13azzqikIgXJEKS1wfPibSg/Wf1JXgDQV7ZKAYQNGdGLd0hQ+3gtbaLtL sp8Q== 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=yBU0HHCaI6zs75ZIaQEg5sXEdmFFNFPA3ed3o1j1hUc=; b=kGVu3TjKL8bSA4ldRgloov+3wlMiK83KowgcVN5U9GWawOx6OIXieQeFoXaOs/Jh5W UBS9Z6gfr5x0kmFXj8AOdBSXPqnnK6j3ruURuN/MWDPClnnihLo8L0G+U0t8ZYZihnI0 r1Ap9vXK74WajnMzji1e0865GCVUfG0nY3CDoSJnAS4mRe2JgPagRa5wPeEHddzeFRZP M32kX9pvxltNgAk2pqrzJXjmWDShz7Hes8kHnk1kss18VXbwEVmWJlAVcSjJmlZcHPnT 0br4MeowUKUM/7U/EVpRXwh519mSve5kLgXnYON0yv4ddcCBILq2ThMMG6BVCAPfAn2p 3i9g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=mZ70M6h2; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::631 as permitted sender) smtp.mailfrom=nicolai.kraus@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=yBU0HHCaI6zs75ZIaQEg5sXEdmFFNFPA3ed3o1j1hUc=; b=MW/b2THPGw3KRj6+mDQvLGZoNvDBsGd6tklG/7+kxcIpmu/ckPeXSCY1Nz5LfPYoLR QF9NjrGdjbiBIjHLJc6oxvQyjr3OGIwvCORJDD5TRwn4eaipwuzkW5k9enjJjgBEhZej G3uULKYSj/Nd0nHTLids+S+DGN3ocp0sIkT7MkbGi5QY8gVoCNoI+Iqp2elL/AgrhAx6 oA16+YxdtdohPG64T8Y3Z42ldBeL9PgAv6QiM+NZdRUrPBN1x1K0Eitro3yT7DuDVOu8 cYWU/y+VRwtLw69NuRZFOI+3b7IAOPislPDmT6rYuOwR4yCPWxoVW40jlX78N7467n4i C2xw== 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=yBU0HHCaI6zs75ZIaQEg5sXEdmFFNFPA3ed3o1j1hUc=; b=byb6Ci8Gm5k/9qznMPTcTlIR6ICPbcQFxGiF6BUo/DJ7z8KNaF31F4vVlgUwA+98yG mkmJaSJ1VsEgskr2ApTgKdZkFhygv3HjaqWbyHt0oximaKYgw4I9/+C0HTRui0lE3JCw SLa0fnEJQB7kycRX6Dnhsf4uOItD5bTdlTZUhBug3Qw1Z78ezTsYFDSxYf0kc+pK0miz HLkbNxrfCpmcD35MLl431/o090uDYZlJBVpuXlq2mbJ1VjtgI6VT+HQ2FwXCuhW24rWe 2+5CgzGLo4q1a3DrY3U2SCAfnAs94Qp68oKtDrYG3OnTqJfLB6ZzqTaqSlvMvwP8kA0S a0Rg== 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=yBU0HHCaI6zs75ZIaQEg5sXEdmFFNFPA3ed3o1j1hUc=; b=fXnis5fzu88VcM/dVODJPHml7C0NhZ5t4lqedq0GiT3GlADGsjQphun5JiWBt3mbs0 rB4wFS+IuR66D05le4FM7YutxwItmYjhJYV5vqsQrNSm3NEJbkGxlw9duh315/ps6PwM 4S6s5EC+UN4Jn6QqxiG3NeA6yMO0Khn7sqHo1mlslnCuecGzeW1WvM/Fwv6pWLvWAf+J g/Q7EQ0UkbtjToXA+x4zu9XT6WAPjxfWZKQzTfUVO6dRAGF6vISX68A7DwNvEzZlMafN AWtZhaVRFqEBRK9JzCMg757eiIbFS01y0CYkiwSXllbxErfQGLCJa5BF4eok9+3Z6FV0 ileQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AO0yUKUjDxDFS3sGrgqtQPpDaW0p5f1Q+/6qOt+naNZl9uFeEMg2+wsw EaA9RVRUnM7m5SAhlZpRdAY= X-Google-Smtp-Source: AK7set9Btz0AbSGvMDjcolDGUKxYldyW5GxPdAgMHv1pM8CuRo1AQa+rg5LZVYXEE2HUH5RTNet92w== X-Received: by 2002:a17:906:3ad3:b0:878:76a1:291 with SMTP id z19-20020a1709063ad300b0087876a10291mr2196993ejd.49.1674919284013; Sat, 28 Jan 2023 07:21:24 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:907:3f1a:b0:84d:4675:1cbe with SMTP id hq26-20020a1709073f1a00b0084d46751cbels5461031ejc.7.-pod-prod-gmail; Sat, 28 Jan 2023 07:21:21 -0800 (PST) X-Received: by 2002:a17:906:b742:b0:878:7557:bc with SMTP id fx2-20020a170906b74200b00878755700bcmr10359486ejb.41.1674919281124; Sat, 28 Jan 2023 07:21:21 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1674919281; cv=none; d=google.com; s=arc-20160816; b=bCEKRLoWkbzGe4FEHHOmVHKeOgb3A23Lziu0FUnycOM9fy/Ibt6GFjJ8CXkRwCKfAz Wkz4QulTFzXwXsX7jt6f8LGeQt7pgoLbTaSjMhQUJ0V82RWH3hz3k8wta8485VmxKyXa gdJFmd3li/ZJpTclqt1P07SRqtMXA0o34LP+ESCXHt9M8DRT+Zafj4iJfgbQvVPmXZP4 gggAwUthPkGFsVC1sywa8cMZD1uQgqiJULyVcJfIDuICkLeSXAEx6DzJkpGfrYrFK+6p hvFX03JTk6wN8SQOF8TH7GLb69QSuJiByRovcUdTLgpwA0262D9Pqy6F6dxW18qDzVZd lxHQ== 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=wHKpITcWYWfwi2vmbH4Hy1h7Qd+/j1/FiY1JMYrDatQ=; b=tIcsN1koZuHczpDOitZDoArAEhrwFoGhtnUDIvO3JQxNHfGQE8BkvwaVxSTIL6lxfI DXYYPfp5w9xLQqLFwSw9nOfB6z03QhHGFa7QYWWXKBEULXig2ERxaTOg3Qr05FWqdgR8 rnP9YWdNz108Xak2ExLQ9JSrrN+nKlIYxKLflBx4XuYw4pmThtMxmY/2Afuj9M6wu80Q MZEpw8aCdzr1/AS3xKrVrr10a0hZrOk9wac55LivXPBt07+oiwxkL2bB6or32HbjcOBR q+1YV3jy0rmIRKHriPKtTiLKHt8uT/kJKPEkyOEWjLiAFTHkSfdK1GfhjH3ObRW2A0En mdZQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=mZ70M6h2; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::631 as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ej1-x631.google.com (mail-ej1-x631.google.com. [2a00:1450:4864:20::631]) by gmr-mx.google.com with ESMTPS id hd11-20020a170907968b00b0087dc2857237si154143ejc.0.2023.01.28.07.21.21 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 28 Jan 2023 07:21:21 -0800 (PST) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::631 as permitted sender) client-ip=2a00:1450:4864:20::631; Received: by mail-ej1-x631.google.com with SMTP id qw12so5028566ejc.2 for ; Sat, 28 Jan 2023 07:21:21 -0800 (PST) X-Received: by 2002:a17:906:2f16:b0:87f:e638:cf68 with SMTP id v22-20020a1709062f1600b0087fe638cf68mr886073eji.281.1674919280581; Sat, 28 Jan 2023 07:21:20 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Nicolai Kraus Date: Sat, 28 Jan 2023 15:21:09 +0000 Message-ID: Subject: Re: [HoTT] Infinitary type theory To: Jason Gross Cc: Michael Shulman , "HomotopyTypeTheory@googlegroups.com" Content-Type: multipart/alternative; boundary="000000000000bf259905f3548896" X-Original-Sender: nicolai.kraus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=mZ70M6h2; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::631 as permitted sender) smtp.mailfrom=nicolai.kraus@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: , --000000000000bf259905f3548896 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 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 this, I don't see how we could have formalised the statement that "Universe Un is not an n-type in a hierarchy 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-ComplicatedT= ypes.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 infinit= ary 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 f= or > 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" sche= me > 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 term= s > 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 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. >> 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/CA%2BAZBBqyc%3DyjbeNbcmdWRXnyyBzaUu3G1x2Mp5cdZA8Asg5oLQ%= 40mail.gmail.com. --000000000000bf259905f3548896 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
That's an interesting observation! However, I think th= e question of universe hierarchies is orthogonal to the question of infinit= ary type constructors.

I don't think access to inter= nal universe quantifications is an inherent consequence of infinitary const= ructors. 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&quo= t; is possible, and it can easily be ruled out. In Section 2.4, strengtheni= ng A1-3 of the 2LTT paper [1], a type theory with such infinitary type cons= tructors is specified without allowing internal universe quantification. Th= is is essentially because the externally indexed sequence of types still ha= s to live in a single=C2=A0fixed universe.

Agda actually= *does* allow something like=C2=A0"=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 found it very useful. Without something like this, I don'= t see how we could have formalised the statement that "Universe Un is = not an n-type in a hierarchy U0, U1, U2, ... of univalent universes (withou= t HITs)" [2]. But I would *not* regard the formalisation [3] as a sing= le 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.
=

Best wishes= ,
Nicolai



On Fri, Jan 27= , 2023 at 8:41 PM Jason Gross <= jasongross9@gmail.com> wrote:
(Resurrecting this thread becaus= e I stumbled upon it while rereading A Formalized In= terpreter, 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 infi= nitary type theory?
I think the answer to this is "it depend= s".=C2=A0 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 qu= antification).=C2=A0 However, infinitary rules give access to internal univ= erse quantification (consider the function `=CE=BB i. "Type"=E1= =B5=A2`).=C2=A0 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 w= ith 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.


On Sun, Jun 22, 2014 at 2:05 A= M Michael Shulman <shulman@sandiego.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://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP= 9wE1t2Y8M7Yi0i1ChYb8PrP_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/CA%2BAZBBqyc%3DyjbeNbcmdWRXny= yBzaUu3G1x2Mp5cdZA8Asg5oLQ%40mail.gmail.com.
--000000000000bf259905f3548896--