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=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-it1-x13a.google.com (mail-it1-x13a.google.com [IPv6:2607:f8b0:4864:20::13a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c7466fae for ; Tue, 28 May 2019 09:51:06 +0000 (UTC) Received: by mail-it1-x13a.google.com with SMTP id g1sf1856986itd.1 for ; Tue, 28 May 2019 02:51:06 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1559037065; cv=pass; d=google.com; s=arc-20160816; b=FrTIQavhQemmETUCNcnFtiuIIAwkN5DAlPCHn9z5oPQXDk9mrDoFRosXBf0Jwvlyu2 JmUfoKL3h29zq+dYiFY9YeYitNEtzcp8bRl8uMzMfTjCHRQgTzxXK/b2NT9RglpAA8nm 1a/QLwrkdDBsoe2eqkAkikvMAGT+XCGKLkMMlnNUvdnb5/khCjANP8CM7HCIC/5ENpX4 +ERILNAWdfhRi3RCEKtWLb+xWb0O4EYn8ev7DoSH1aG+uI9OLAZhAplnsP7jQmmc9gAF bYX0OMzPmb88TVT3y6jQK1grCcFjBe0cLhsVppPf+rBe44EZwGzTyz6GG+W4+hFBjKno C3Yw== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=VIctPjIY0is/9l3mMEoNU/MAhbb+psTOZxU+6F65F6M=; b=nP0h4b9todvE46XVaQaluypdkLW0IAOeg7+Knq6RbH940NooXqrom77nBP5T7WOxyG fGWczTGFVpCm5qulegwb3V3x17ioVMnVGysm7T1jkTKwBPcmUjGaohc38mipLyimZSfQ r5WwcBceFoQp1+fArvMs+56JEzVewN1b71ZMf3565JRenZ8AMeiAOGOck1Bq5Gfm/+OX gLHHSXXE+i/r3abMJo10rtvkAPmMmX2icnYx5gZ5fqNKfMQelIbUzOJlftay5r0qosHC rEs2vKjlpJSPYqXA+jrIdyEo134tS1KETnCNOEdkt6e4VQOC7bAy/3IUoUUus7zhspal 6oqA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=j2seQQzS; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c31 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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=VIctPjIY0is/9l3mMEoNU/MAhbb+psTOZxU+6F65F6M=; b=jH4A6+ReYMWGSM++2ChFRhSNCLwsCqPtBTvEgd98q68wie0L+Oadahb6jCb5Nc8bfv 9kNbn4nWNNtGn8ebG2nhFwgojZkjEMPsOK29FClue3irp1gK8tdOaT0HL6MG4ybdFbCK 2KTjPUEhysz9LUQwFSsym5AhVdKb57+zM1S2CIR02Jz2DxgUROV7uMzXXontX5rSYLC3 ht9JZgPES6EjglDJkzx+EmkJBX4kVuBH9LzinifoKXrNCpGB6Fhvt4q8rUKJnUDoHQ0b ZYZKjHyJVOKzVdeH9BMWAmK88zI1mpQ3ZAYtWQ4t3JRp7Wn8QBnB3tsuqaeVrf5HrYPf RGpw== 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: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=VIctPjIY0is/9l3mMEoNU/MAhbb+psTOZxU+6F65F6M=; b=s1v4TV3KheRrHzLYkaeYe/rbO0OWmDFB59FyHt2uZVD8qHdy1crpaGEp1h3nU9Bryv ycIoXy/pw/jJvC0hBsTM5qcHUzl86nd4Yq1YujxRpblRM4jg7nweYBRSRPc+sGE+84I3 7dImd9P/TFv8ydzbVzEGYovrWjttR0hLp5DNYAvtdoqY4sGawct3kMek/FSzkXkXzOZm gRkoAUBWpuMJ33ed7X0VkvrvCLQ0Y9UlExxATBxSivhowhBJkVNDJTgam1NqIXXrQ37C r+iEc7ueQmHAZb7q5ugkgRoMQCG6clMAlaSaeNEFkViOlEdRyy5rM/y+Um2KyLDOb4Rk tR5g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXj9mYvNXhlTr3lHeKg0IfoyXzFwGqxhfqC/G5Pxrwjh8ZrcIXh krmqoywgHztPEUQODqxJj1U= X-Google-Smtp-Source: APXvYqzmRaCrRXFlIr/8/sSBC5Lfj8iVRXKusWjDbe7whAgp9W2vR62z+bYANL/SsSYZSmkkrulj8Q== X-Received: by 2002:a02:3217:: with SMTP id j23mr23673248jaa.79.1559037065379; Tue, 28 May 2019 02:51:05 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:660c:f81:: with SMTP id x1ls568535itl.1.canary-gmail; Tue, 28 May 2019 02:51:05 -0700 (PDT) X-Received: by 2002:a24:91d2:: with SMTP id i201mr2536840ite.88.1559037065031; Tue, 28 May 2019 02:51:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1559037065; cv=none; d=google.com; s=arc-20160816; b=ZTfC3NrWY0i4kvX7KsPnv/TtAqNg3xj2gg1h+liSDHLcrQyB7mX8ssT0AP/Lir/+qe 9RYsGXEpwOE2CrqsdtjB49izStKfAdPY0KXnz6QoQEROMbq6+bmXuH2wI3o3cWX247bO +HMJzCzjfqzku9V+HLnTnLP0BMzGX4dzxh1pb5aBNHsDHr++FytYYDjnIYD3FqJS2K9y 0WOj95qTeSoWaS87A6AzxyuVp829AtmH8dA9cQI3VPaBAqzIIgox6nH04P/AUui4eWEj PL9pAzjPK7egSxrMUZc2IDjjpHIIfOsc9LqtnJIrV7JQdLONfc0TjdUmujXH2DUoB4Z9 REvw== 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=WlG9HGllk4vZuyqgYa/6al72xrxY7/xJomwwZ9+IMPU=; b=sqwpFZWdqx+6XVVXXgHsljgbCe3QnEWQqCPsAEBzQIxk7g3g06WzvWmeJXt96tr/Ix q2ulr8o9zhWJVB9W6fSIL3PNXg8j9sMjxGrx7UjmHlmX4IcKTnN8s80eaJauvqvrEd2D QIH38v5CrQzjJGeJzrrbedo87ux56Twc/dboeNXWDW2a4AfYMYgUCyh9fuHJPmQSNMw3 TpruD6kOr5ekR4qsZZsYpOjyoMO97EMuTsNdNKOP31jcE6itdNDJbeJl7e4QXxc+q1SM uIDIc7zakUzCltrUrkwh2ibwblT+sdLNw3LYzrnRhDmSwN6AGyDplvvz/u68f2eld80i l50w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=j2seQQzS; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c31 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc31.google.com (mail-yw1-xc31.google.com. [2607:f8b0:4864:20::c31]) by gmr-mx.google.com with ESMTPS id h19si51851ith.2.2019.05.28.02.51.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 28 May 2019 02:51:05 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c31 as permitted sender) client-ip=2607:f8b0:4864:20::c31; Received: by mail-yw1-xc31.google.com with SMTP id w21so7656533ywd.6 for ; Tue, 28 May 2019 02:51:04 -0700 (PDT) X-Received: by 2002:a81:5145:: with SMTP id f66mr59016173ywb.195.1559037064318; Tue, 28 May 2019 02:51:04 -0700 (PDT) Received: from mail-yb1-f170.google.com (mail-yb1-f170.google.com. [209.85.219.170]) by smtp.gmail.com with ESMTPSA id a127sm3577745ywh.3.2019.05.28.02.51.03 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Tue, 28 May 2019 02:51:03 -0700 (PDT) Received: by mail-yb1-f170.google.com with SMTP id s69so7432476ybi.2 for ; Tue, 28 May 2019 02:51:03 -0700 (PDT) X-Received: by 2002:a25:c983:: with SMTP id z125mr54681392ybf.45.1559037063421; Tue, 28 May 2019 02:51:03 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> <3f6331a7-688e-570b-01d8-d02a81eac96b@inria.fr> In-Reply-To: <3f6331a7-688e-570b-01d8-d02a81eac96b@inria.fr> From: Michael Shulman Date: Tue, 28 May 2019 02:50:50 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Kevin Buzzard Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" 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=j2seQQzS; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c31 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: , In my opinion there are several separate issues standing in the way of a wider use of proof assistants. One has to do with the design of the underlying formal systems. In this respect Book HoTT (the formal system of the homotopy type theory book, with univalence and higher inductive types added in an "ad hoc" way on top of intensional Martin-Lof type theory) is a step forward over systems such as CiC and MLTT on which Coq and Agda are based, due to various factors such as a nice treatment of quotients, automatic isomorphism-invariance, inductive and free constructions, etc. However, Book HoTT is also a step backwards, because the presence of non-computational "axioms" means that "execution" gets stuck whenever you try to use univalence. So you can prove automatically that anything true about a group G is true about an isomorphic group H, but if you then try to take some specific statement about some specific group G and transfer it to a specific statement about a specific group H along a specific isomorphism, what you'll get will be an unreadable statement littered with explicit transports across univalence-induced paths in the universe, rather than the "real" statement about H that should be obtained from actually *applying* that specific isomorphism. (To be fair, plenty of people using a system like Coq pre-HoTT had to add their own axioms, such as function extensionality and UIP, and when you want classical logic that's unavoidably an axiom. But at least the underlying type theory of Coq and Agda can "compute".) More modern homotopy type theories, which are generally based on cubical structures, allow univalence to be "executed" by the system. However, these systems lack (so far) all the intended categorical semantics (see below), and haven't yet been implemented in "real world" proof assistants (though there are prototypes now in use and development). In addition, as Noah mentioned, two-level theories with a stricter kind of equality (which do *not* exist in UniMath, HoTT/Coq, or HoTT/Agda -- this point is about having two different equalities on the same type, not two different classes of types with different equality behavior) are likely to make many things easier, but haven't been implemented in real-world proof assistants either (apart from some sneaky coding with typeclasses). So overall, I would say that the underlying design of homotopy type theories is not yet "in order" to achieve its hoped-for maximal benefit in a proof assistant by the working mathematician, though there are promising signs and progress is being made. All the issues discussed above are what I would call "mathematical", or perhaps more broadly "theoretical". But a separate issue standing in the way of wider use of proof assistants is what I would call "engineering". No matter how fancy we make the underlying formal system, I believe it will always remain true (for the foreseeable future) that a proof assistant needs a lot more detailed information than an ordinary mathematician would care to provide, or need to see, in writing and understanding a proof. This is where we need things like tactics, implicit arguments, elaboration, proof automation, etc. to fill in the gaps and make the system usable in practice. Here there's been a lot of progress over the past decades, but I think there's a long way to go too, and choosing a better underlying foundation (like any form of HoTT, cubical or otherwise) may improve things a bit but is not really a game-changer. However, there's something completely different that I do believe has the potential to be a game-changer. There's already a very different "gigantic wave crashing through mathematics": homotopy theory and higher category theory. Homotopy type theory gives type theory and formalization the potential to ride that wave. The real point here is that when something is formalized in type theory -- constructively -- it is automatically true internally in all models of type theory, and for homotopy type theory those models include higher categories. Note that the use of constructive logic has nothing to do with any philosophical belief; classical logic can still be "true" in the "real world", and yet constructive reasoning is valuable because it makes a theorem true internally in more categories. I think it's fairly hopeless to convince a classical mathematician that they should put in a lot of work to convince a computer of the truth of *something they already knew*. But I have much more hope of convincing them that they should tweak their proofs slightly, and perhaps use a computer to help verify the validity of the tweaks, in order that *essentially the same proof* will allow them to conclude a *vastly more general theorem*. Moreover, when working with higher categories the advantage is even more pronounced, because homotopy type theories introduce a totally new kind of proof that can be much simpler than all the previously available options -- and the immediate feedback involved in using a proof assistant is one of the best ways to *learn* that style of proof. In short, I think there's a huge public relations opportunity here for type theory and computer formalization, which sadly even Voevodsky missed out on. Rather than selling it as a way to be absolutely sure of proofs we already believe in (as important as that might be), we should sell it as a framework for *entirely new proofs* that bring the otherwise fiendishly complicated and technical world of higher category theory "down to earth". The experts in higher category theory are familiar with the fact that in many respects it is "more natural" and "better behaved" than ordinary category theory; but there are thick barriers to entry preventing many of us from getting to that point of expertise. With synthetic mathematics in homotopy type theory, we can envision one day teaching higher category theory to undergraduates. -- 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/CAOvivQx_b2QkEL-HqMXQNJ_QA83KjdAnFe7RmmiPRRQX6tYk-A%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.