From: Michael Shulman <shulman@sandiego.edu> To: Kevin Buzzard <kevin.m.buzzard@gmail.com> Cc: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com> Subject: Re: [HoTT] doing "all of pure mathematics" in type theory Date: Tue, 28 May 2019 02:50:50 -0700 [thread overview] Message-ID: <CAOvivQx_b2QkEL-HqMXQNJ_QA83KjdAnFe7RmmiPRRQX6tYk-A@mail.gmail.com> (raw) In-Reply-To: <3f6331a7-688e-570b-01d8-d02a81eac96b@inria.fr> 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.

next prev parent reply other threads:[~2019-05-28 9:51 UTC|newest]Thread overview:31+ messages / expand[flat|nested] mbox.gz Atom feed top 2019-05-25 10:12 Kevin Buzzard 2019-05-25 10:22 ` Steve Awodey 2019-05-25 12:23 ` Kevin Buzzard [not found] ` <B7D67BBA-5E0B-4438-908D-4EF316C8C1F1@chalmers.se> [not found] ` <CAH52Xb1Y=Xq=012v_-KSDUuwgnKpEp5qjrxgtUJf+qc_0RWJUg@mail.gmail.com> 2019-05-25 13:13 ` Fwd: " Kevin Buzzard 2019-05-25 13:34 ` Juan Ospina 2019-05-25 14:50 ` Noah Snyder 2019-05-25 15:36 ` Kevin Buzzard 2019-05-25 16:41 ` Noah Snyder 2019-05-26 5:50 ` Bas Spitters 2019-05-26 11:41 ` Kevin Buzzard 2019-05-26 12:09 ` Bas Spitters 2019-05-26 17:00 ` Kevin Buzzard 2019-05-27 2:33 ` Daniel R. Grayson 2019-06-02 16:30 ` Bas Spitters 2019-06-02 17:55 ` Kevin Buzzard 2019-06-02 20:46 ` Nicola Gambino 2019-06-02 20:59 ` Valery Isaev 2019-06-04 20:32 ` Michael Shulman 2019-06-04 20:58 ` Kevin Buzzard 2019-06-06 16:30 ` Matt Oliveri 2019-05-27 13:09 ` Assia Mahboubi2019-05-28 9:50 ` Michael Shulman [this message]2019-05-28 10:13 ` Nils Anders Danielsson 2019-05-28 10:22 ` Michael Shulman 2019-05-29 19:04 ` Martín Hötzel Escardó 2019-05-30 17:14 ` Michael Shulman 2019-06-02 17:49 ` Kevin Buzzard 2019-06-04 20:50 ` Martín Hötzel Escardó 2019-06-05 17:11 ` Thorsten Altenkirch 2019-05-28 15:20 ` Joyal, André 2019-05-27 8:41 ` Nils Anders Danielsson

Be sure your reply has aReply instructions:You may reply publicly to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the--to,--cc, and--in-reply-toswitches of git-send-email(1): git send-email \ --in-reply-to=CAOvivQx_b2QkEL-HqMXQNJ_QA83KjdAnFe7RmmiPRRQX6tYk-A@mail.gmail.com \ --to=shulman@sandiego.edu \ --cc=HomotopyTypeTheory@googlegroups.com \ --cc=kevin.m.buzzard@gmail.com \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting theIn-Reply-Toheader via mailto: links, try the mailto: link

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).