From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.8 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pf1-x437.google.com (mail-pf1-x437.google.com [IPv6:2607:f8b0:4864:20::437]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b9e358ad for ; Thu, 20 Jun 2019 16:56:31 +0000 (UTC) Received: by mail-pf1-x437.google.com with SMTP id y7sf2399163pfy.9 for ; Thu, 20 Jun 2019 09:56:30 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1561049789; cv=pass; d=google.com; s=arc-20160816; b=NgLZet6Oli0YTO+gRqEcEPSklEo260bGCJsa3DIe6NK4fVkjpU6vudEQvalJIHk26Q imMRYbqbWCcQzJpWXljfL+tyGFyFPTdOztktEJ8V9jgLhjmUGhrPXGOhj0g4UvvFi8bB sSbTJ5ir+lHKNyfbGI3RqgWsfFLoMHLgELtPxhJMRES461w70urGqQTkTXiRkOjaJfXH EgrNoAP0tzhuWPL29KKLc1R9abybrhWYjUMwsfqe3Na/+6+/yn/OmPdFVDsl5f91q4sJ oxWMq9Bp0EDfqBbkbG5fahe1KGjdWJC65SP5NA+94xiJZemm9dZvV4L/cXnb7HCLFSjS vHZQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe: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=wgK0t4Y79Snb/NSiJFb+IK+hS0x4kV9FZlBjNI3bCz8=; b=r/03WnGbm8cBslWWg39z6J3KtV0un40lp9wfGPyL3qxeKjNb9tE0lS1NEzR+ts9I9m n87aNfne+6MLQILpoucU0j4Xs1KTWAvTf9mJseccjvwACEfOFZkBPr98+WR9KySRPA4f xlZl34QVzQZE9YbGYRhPi0ay40sd8WOSQgoxw9AYNU3SzfhRgT/20Gch5baTd+1pWKT5 OBCr1nJ8Nq/UdUJiV3KK9CY79cNfLpd5MBawrXUlR/XOQmdkywM0lgyUZYe5/QkFRnKo B+GqfX91UCYAnuq9mdsTXB5mo5uKRg0Xs0dUVHiNxBg6fWLFVeibpNM2nL3ySsTOT0jd 0ycQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=nHy8kur+; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c33 as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=wgK0t4Y79Snb/NSiJFb+IK+hS0x4kV9FZlBjNI3bCz8=; b=JHZgd8aQTQNn9m1DUNqSx1R6tv8xJS5p1tlskDB3mudUImiOqUDrv9zxjYX8kgXsSy B324wiA+VWgnT0dzfBqIP1p/zgLDiSGP2YfSTl49IplNP82uocBEA0WoF+q0WEAGoaCa dGkzlldkImmBBnh0BNbG4CY2ZOOOi9KCW6D43LwxKszDozj141+oeZLVMK49B65Hu3Dm rYcwe0tY0sLADnhK0l2zaE3E8kxnyIQFdUXgGnd08fOa0xxk02XlnflPM3ucS2AQ8N/7 mnUuBrSGbRyFsHHie/y13mI49gjQRrfmUrhGAkQ3b5Zz/MVAlIhot6u2rFCh6K8fpvHm 1HqQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=wgK0t4Y79Snb/NSiJFb+IK+hS0x4kV9FZlBjNI3bCz8=; b=pobUJ6aj5mYLLJBr49RD3TwcxkEtAXbdO2N1t1boRK1/mZMzbhlJwwOpsrIJxag11/ Qui9EC6KGBPqksbclotaqPlAH/7DgyOoUJHtn5qRkNrGd2vLzn/JGvHtHSLDIQo1bzBm eCvjfoFAJXiCs4H/ezgJ59Gb6bYrz657NsJp+SitjJ7JMGhW+cPzp1s9UQbyzly10ma8 qFkPYeGd7HMplzmtzKh1gUnfC8WLVddbeCY4D7G6Dnhby0yeiBwo3QtTR627fryLvnMZ upm3D+YdPM6je2fppiYhv6GgewlKFR2RxWFZ5pnsIndlFxs1ISokw0uKgPuOfNiy4eMD +wZQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWyL6rJppNXCeUuqvVa9zOKUC71woaWkgBaQZSOkB+pmSp9b9dy d8Mo/cWlzJNLqQtTvTbizHI= X-Google-Smtp-Source: APXvYqx2ks3TL9p5YSU6MQV+1PcwcXexxwUtgCpMBW/VlIJwZetMYq88TIMXCQBpAVnmxlE78SIv9w== X-Received: by 2002:a63:5065:: with SMTP id q37mr13714398pgl.32.1561049789671; Thu, 20 Jun 2019 09:56:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:5ec4:: with SMTP id s187ls1453747pfb.1.gmail; Thu, 20 Jun 2019 09:56:29 -0700 (PDT) X-Received: by 2002:a63:296:: with SMTP id 144mr13924059pgc.141.1561049789178; Thu, 20 Jun 2019 09:56:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1561049789; cv=none; d=google.com; s=arc-20160816; b=O/5h0LckxYi/FbS/QM39jsub50sKfIVpMngSd+yDWY2WN8bVBke+Ohmtj7OCyO8hY7 ZRiHJ9fIcAq5EzfdE3hnL3MWGPgdXMLwqK7ZpNdu5mU1KR8iWg2+aJngvfW/dMRAbMvW ujHmRlnaToFFBoArR+i3liKXarl5V0d+2xRcQipOexoagTxJ5jVapoFUxDUsAqjq7Mhu /a4BICe+InQx/Z6qYS7ZPHZO2fObjwpC3unCXl3ZNgYvzbqYrmNjUV8vun4pMLDs7w8a +rUhTq3Qk1bNoaUR7wbo9QFnyaIIYizFBWGYH0kC5rhsAyxoEdDLpIKe2TCzWv/PAvJp 0SAw== 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=rwyVh+27uQpEZTW5ebOy1Szlfk4BihI9xWzKMYqGAkI=; b=01/hG/kQlKs9tN+paBMmIJeeI8VFgt01anSBKjgpDwnOVrSU7YBI9uUzlBisjc1Pt1 q45KruOYQzHwhSC+GUHq1gm+XWiHPg49MrSFDD/eIYyEJzdC4Nan3CiSXuLLmjYJFG56 1ZRtcfadBm89ZBeobozve359BGLiFCqc6nbgrDPuGSvNmLY1d36W1gAA+fO6/lL4WV6S VnuX/tWLeMfnvxN64XRvy5fNNFN6q1hbWveHzOUnT0LUnHsKAbTHbc/oZNNfLvdH0XG8 NOa9JXRKnU3kaXROPy6FvdQ5o4k7AHM+cAG8UkKzSaZ+6CioIRg6CadEh1FqEOzxoGjO 3jxQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=nHy8kur+; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c33 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc33.google.com (mail-yw1-xc33.google.com. [2607:f8b0:4864:20::c33]) by gmr-mx.google.com with ESMTPS id d128si4932pgc.5.2019.06.20.09.56.29 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 20 Jun 2019 09:56:29 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c33 as permitted sender) client-ip=2607:f8b0:4864:20::c33; Received: by mail-yw1-xc33.google.com with SMTP id l79so1452260ywe.11 for ; Thu, 20 Jun 2019 09:56:29 -0700 (PDT) X-Received: by 2002:a0d:ccc6:: with SMTP id o189mr35264721ywd.450.1561049788188; Thu, 20 Jun 2019 09:56:28 -0700 (PDT) Received: from mail-yw1-f48.google.com (mail-yw1-f48.google.com. [209.85.161.48]) by smtp.gmail.com with ESMTPSA id e14sm65707ywa.23.2019.06.20.09.56.27 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 20 Jun 2019 09:56:27 -0700 (PDT) Received: by mail-yw1-f48.google.com with SMTP id s5so1456726ywd.9 for ; Thu, 20 Jun 2019 09:56:27 -0700 (PDT) X-Received: by 2002:a81:35c9:: with SMTP id c192mr66436612ywa.193.1561049787308; Thu, 20 Jun 2019 09:56:27 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Thu, 20 Jun 2019 09:56:15 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] my first 3 questions about HoTT To: Thorsten Altenkirch Cc: Nathan Carter , Homotopy Type Theory 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.20150623.gappssmtp.com header.s=20150623 header.b=nHy8kur+; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c33 as permitted sender) smtp.mailfrom=shulman@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: , On Thu, Jun 20, 2019 at 9:39 AM Thorsten Altenkirch wrote: >> Very early in the HoTT book, it talks about the difference between types= and sets, and says that HoTT encourages us to see sets as spaces. Yet in = a set of lecture videos Robert Harper did that I watched on YouTube (which = also seem to have disappeared, so I cannot link to them here), he said that= Extensional Type Theory takes Intuitionistic Type Theory in a different di= rection than HoTT does, formalizing the idea that types are sets. Why does= the HoTT book not mention this possibility? Why does ETT not seem to get = as much press as HoTT? > > ETT or computational type theory relies on some notion of untyped computa= tion which is then sorted by defining some semantic criteria for types. I don't know what Harper was talking about in those lectures, but although he does often talk about computational type theory that assigns types to untyped computations, usually "Extensional Type Theory" refers not to that, but to an intrinsically typed theory like HoTT that contains a "reflection rule" saying that any two typally (nee "propositionally") equal terms are in fact judgmentally equal. In particular, this forces all types to be sets (i.e. 0-truncated). The HoTT book doesn't talk about this possibility because, well, it's a book about HoTT, not about ETT. ETT (with reflection rule) has an important disadvantage that its typechecking is no longer decidable. There have been some serious attempts to work with such type theories (e.g. http://www.andromeda-prover.org/), but there are also several other often-preferred approach if you want all types to be sets, such as assuming Uniqueness of Identity Proofs as an axiom (or an equivalent axiom such as Streicher's K), allowing unrestricted pattern-matching as in vanilla Agda, or fancier things like Observational Type Theory or the recent XTT (https://arxiv.org/abs/1904.08562). There's nothing wrong with these theories; they just serve a different purpose than HoTT. Indeed, such theories are sometimes combined with HoTT in a "two-level" type theory (e.g. https://arxiv.org/abs/1705.03307). > There is the remaining issue that it is not known whether the cubical the= ory coincides with the simplicial interpretation which is the standard one = in homotopy theory. I would express the issue by saying that it's not yet known whether cubical type theory has all of (or even any of) the intended higher-categorical models. The simplicial interpretation is only one of these models. >> One of my favorite things about HoTT as a foundation for mathematics act= ually comes just from DTT: Once you've formalized pi types, you can define= all of logic and (lots of) mathematics. But then the hierarchy of type un= iverses seem to require that we understand the natural numbers, which is wa= y more complicated than just pi types, and thus highly disappointing to hav= e to bring in at a foundational level. Am I right to be disappointed about= that or am I missing something? As Thorsten said, you won't get much of anywhere in mathematics without the natural numbers in your foundation. However, I suspect your disappointment has to do with the occurrence of natural numbers at "meta-level" to index the universe levels, rather than the natural numbers type that appears inside the theory. For comparison, note that ZFC has in fact countably infinitely many axioms, so it also involves some natural numbers at meta-level. However, it is nearly always possible to eliminate such meta-infinities by incorporating them into the object theory; for instance, ZFC can be replaced by the finitely axiomatizable NBG, and one can formulate type theories that "internalize" the universe levels. For instance, in Agda there is a *type* of "universe levels" over which the universes are parametrized. Our semantic understanding of such universe structures is currently fairly primitive, but I expect it will improve. --=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/CAOvivQzgvD8sqxbxn_2xOXQZ1XoSG4vnEe8LhcaQt_G2H8C6SQ%40ma= il.gmail.com. For more options, visit https://groups.google.com/d/optout.