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-ot1-x33a.google.com (mail-ot1-x33a.google.com [IPv6:2607:f8b0:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 34498d9c for ; Tue, 28 May 2019 15:20:04 +0000 (UTC) Received: by mail-ot1-x33a.google.com with SMTP id w110sf10451378otb.10 for ; Tue, 28 May 2019 08:20:04 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1559056803; cv=pass; d=google.com; s=arc-20160816; b=0Z6JG0+bn+Gn8imBBPY5BXhFHaJEpnHQytLKAD1Gs2JzkDynHVt9yF1YPuYHSfnd6r GgB4SCnUibrvuFbtuTGd1P4C0cu0jq0+OYBGAUCUCZvbvApFIsAUV1eS87NIqP6lpkH5 xjuWpmZ85w9rXhuardewYLek5Z2m2KV0HCbgCiZFUbS4hKMg3bbzjZBu4G9wUqUFS2OL 9jQFIsY7H8UbRZAm8cYCS3lTXR0puLzCOTn77yUAByTEU1gj8YKS/iqByix/jRo6WMyg eB+CnRhFlL3PRPDfLTjqA1xuPPvt93PQ7inMF5ldtg/+D5OZxK7W3XJU3RydtSdx68vd 6Hiw== 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:mime-version:content-transfer-encoding :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from:sender :dkim-signature; bh=J0j5xjIGa7DbTtYZM7414NfSSMuiXE4TWZOvQq8Hmek=; b=vPfnF5nnUd9tjUqM8Fepxn7DV4MVkcKFtR0bor7MMuXj6Ph9JTTG5q4pf6lcMDNRIh uFEH21AUQHuPKyt/OIXtZ7FslYSnMP3vvptwHQ1bw8lxwD2z/Xj06OJhwJ1G4kmPqde3 il2Olj4y43dZ8k3yVKijGjN/kUnIH+kp/eLcke6fxxv1FeWyjwBDLQ4nwaeT9xx2dwJ4 8+HKXwtY3woJi0sSJVHocDhnUTEBtKBQAauZ43ulFUeVj6QxZOVjwKeXkqxMW+OJr2Wv d6dXpMcyAxe1UBWPv78n0ilNM7yWedYSWvpbb1ZQCrVYoFZZRcMImryhdpURFhPGippi /O3Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of joyal.andre@uqam.ca designates 132.208.246.162 as permitted sender) smtp.mailfrom=JOYAL.ANDRE@uqam.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language :content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=J0j5xjIGa7DbTtYZM7414NfSSMuiXE4TWZOvQq8Hmek=; b=gaWi7iqvewwevPvzQzRBu94HsjrbGXfCO+Ih5cWRy6oYbkJ9djuGEeHjo5DRgqUKzC 9FjTsgsF0bw2lwWNG5Qm1cvsN+ZfLlu84dcx7cV/ZJQY7YBB+65/T/iITuaQmv8JdI6e IpalKO8WayEOtXX3Y+ojNPjiUDc59PguF082IU0SY1088blF8i+wnHIHt04XiiGwjp6d ukpU9vUPfEYlxlBPjpi8ion0QZE1JN3cUQxm+miich5oMRaEm5ij8OYh+tDCHQosXmCB pvu1f2pCvex5rRPOt1ISCjOAMvK48OfniCWTVBdax0nvJwcYs3Fq0BtP8vWj5lVNDgcQ T+wA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:content-transfer-encoding:mime-version :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=J0j5xjIGa7DbTtYZM7414NfSSMuiXE4TWZOvQq8Hmek=; b=EaYYzn1AkxtswXIkjAQkDVURS1OMycs/zUBgTEIKToTbgSyCH4MmQEpLBkkms7AjUR Jj10s/QI8iUfCHSMUTWg5NxR/olBnDXKJdTjGQ+6sSpn23okNxUeLUnYtKSduhqUmarn KxRYptheNIOndG9vEIDK7b87UIrM73/cKyHY6pm2Ky0zhiGgSxEI68grM8COOQcSgIpN lvYD3nWbg3jRoYpXBz/DPWxfOXhR5Q/V+Hf7+vX49QLYfDiOxhO8t4wYDXxEXAGotrax Uc+UDMGNOrN4uaFQ4jlxxeDLe2dFJ5GhoLxSacXVGRBsGborqyORWyppWlwsQxgTPgvl V5jg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXujUHWO4dpgCQ9vo41fZGy7WFaZNhKia6urruoelW40p5o0imk RUeSPXpouJ2zl41QoAIcBgU= X-Google-Smtp-Source: APXvYqy0CxNfeRUoZ8jaqyznbU86LqBhoCC/tepK3Nw8kYYA9PPXxwR1TA8Ki2G+Gc7wxS7CVw7j3A== X-Received: by 2002:a9d:6481:: with SMTP id g1mr31445964otl.138.1559056803369; Tue, 28 May 2019 08:20:03 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:63da:: with SMTP id e26ls3527064otl.14.gmail; Tue, 28 May 2019 08:20:03 -0700 (PDT) X-Received: by 2002:a9d:74c5:: with SMTP id a5mr1374108otl.322.1559056802988; Tue, 28 May 2019 08:20:02 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1559056802; cv=none; d=google.com; s=arc-20160816; b=Km+XHbGNwoj29f94JzSsbQoHjTwgh5HxhpmTdZ3LMLsLcGUyzhxKhimgHMI9BoI1Da 7entvweBzMzRijDBwQE7CCSNp7TudVeVyPwD254Suntj3AOcvEZSYCkDR62NDLqhUAnW pWziTJv9BucfvBvz9fV1k6+cDJrC7//B3BwW91S7h0ywNs4UlYEvulLRPqC53rTEH8lr JxJpa94DOgmHFsw9ZEEKLAgIKvOII0Z4Homiw4+qTfky2yXK1T6Yllk9TwFco4OWT0dr NXEYQRdbzAwX+rRRmbx/VOxaA3G5BPjFeRnhIB0O3VnxICgWiJiOcIYMAguX61VW6YJW Um1g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from; bh=E2i1EwCvLaj4TD9N1fLEeooWj9QSAqLgFPjj65qbRos=; b=0EmfpAoKb0e7Jb68cPJ111UCJ3zQEHMm0CFte89wj1H47ervr2TJmLoVSyKmnzN2Wj Y0pJq8Q2BeqjZJnVtHRfqKKrg/UYQ673KAn4Ot2wKFgZd7aZTH0Ttk4j5ffsjsKpaqmE /XxubFNjgUWF68s1tK0gQGHBPmTlIviuqj9PgyBdle+gEiRc2F/PZXiJbELvdqupoZLY RuzoFN8lDbgLhcS8b9ijNAHAC0a1baoXCWUPm1Zu12LIaEV2Q0cYqTipVfxeWhNRF6Z0 YUpCDiLnufbLzUCluLMsBEUGVDZv/6Jq/XTR4Tc1QXhXNJiEgzrI4GbxcDGAAnzJgiz1 bWyg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal.andre@uqam.ca designates 132.208.246.162 as permitted sender) smtp.mailfrom=JOYAL.ANDRE@uqam.ca Received: from data.crochet.telecom.uqam.ca (mail3.uqam.ca. [132.208.246.162]) by gmr-mx.google.com with ESMTP id l18si813831otn.4.2019.05.28.08.20.02 for ; Tue, 28 May 2019 08:20:02 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal.andre@uqam.ca designates 132.208.246.162 as permitted sender) client-ip=132.208.246.162; Received-SPF: None (data2.crochet.telecom.uqam.ca: no sender authenticity information available from domain of joyal.andre@uqam.ca) identity=mailfrom; client-ip=132.208.246.209; receiver=data2.crochet.telecom.uqam.ca; envelope-from="joyal.andre@uqam.ca"; x-sender="joyal.andre@uqam.ca"; x-conformance=spf_only Received-SPF: None (data2.crochet.telecom.uqam.ca: no sender authenticity information available from domain of postmaster@Message.gst.uqam.ca) identity=helo; client-ip=132.208.246.209; receiver=data2.crochet.telecom.uqam.ca; envelope-from="joyal.andre@uqam.ca"; x-sender="postmaster@Message.gst.uqam.ca"; x-conformance=spf_only X-IronPort-AV: E=Sophos;i="5.60,523,1549947600"; d="scan'208";a="319577304" Received: from unknown (HELO Message.gst.uqam.ca) ([132.208.246.209]) by data2.crochet.telecom.uqam.ca with ESMTP/TLS/AES256-SHA; 28 May 2019 11:20:02 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.178]) by Message.gst.uqam.ca ([169.254.1.159]) with mapi id 14.03.0439.000; Tue, 28 May 2019 11:20:01 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: Michael Shulman , Kevin Buzzard CC: Homotopy Type Theory Subject: RE: [HoTT] doing "all of pure mathematics" in type theory Thread-Topic: [HoTT] doing "all of pure mathematics" in type theory Thread-Index: AQHVEuJPXRED9oDxpUe1rGDNMQ2KjKZ75NWAgAA1u4CAABULAIAADOgAgAASRYCAANxQgIAAYg2AgAAH8wCAAaL2gIABWuUA////fxE= Date: Tue, 28 May 2019 15:20:01 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B15872D76E@Pli.gst.uqam.ca> References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> <3f6331a7-688e-570b-01d8-d02a81eac96b@inria.fr>, In-Reply-To: Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.80] Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Original-Sender: joyal.andre@uqam.ca X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal.andre@uqam.ca designates 132.208.246.162 as permitted sender) smtp.mailfrom=JOYAL.ANDRE@uqam.ca 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: , Dear Mike, I would like to add my grain of salt to the discussion. I think that mathematical research is more a communal activity than we thin= k. What is considered a proof largely depends on a consensus developed within = the mathematical community. Of course, the consensus relies on the opinions of experts and specialists.= =20 Publications and referees have an important role. But there is also a mathematical culture based on knowledge of abstract ide= as and the mastery of symbolic computations. Homotopy type theory is contributing to the present mathematical culture by= bringing=20 a new formalism and new abstract ideas. It claims to be constructive and general (everything is a type). There is an old philosophical debate concerning constructive mathematics that was initiated by the work of Cantor, Kronecker, Hilbert, Brouwer and B= ishop, to name a few. It is true that a constructive theorem is in a sense better and more genera= l. In reality, constructive and non-constructive mathematics are the two faces= of the same coin. The latter is feeding the former with results to be proved constructively! It seems obvious that the debate will endure for many generations to come. I believe that the contributions of homotopy type theory to the mathematica= l culture are important and real. It is worth developing abstractly and for the purpose of creating user-friendly powerful proof assistants. The language of type theory includes parametrised objects, sums, products, = universes and univalence. It is not incompatible with the language of category theory and of homotopy= theory. Hopefully, the three languages will be combined. Best, andr=C3=A9 ________________________________________ From: homotopytypetheory@googlegroups.com [homotopytypetheory@googlegroups.= com] on behalf of Michael Shulman [shulman@sandiego.edu] Sent: Tuesday, May 28, 2019 5:50 AM To: Kevin Buzzard Cc: Homotopy Type Theory Subject: Re: [HoTT] doing "all of pure mathematics" in type theory 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 e= mail 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%40ma= il.gmail.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/8C57894C7413F04A98DDF5629FEC90B15872D76E%40Pli.gst.uqam.= ca. For more options, visit https://groups.google.com/d/optout.