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.9 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-vk1-xa40.google.com (mail-vk1-xa40.google.com [IPv6:2607:f8b0:4864:20::a40]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id af2ff2b2 for ; Tue, 26 Nov 2019 22:18:50 +0000 (UTC) Received: by mail-vk1-xa40.google.com with SMTP id x65sf9602146vkd.15 for ; Tue, 26 Nov 2019 14:18:49 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1574806729; cv=pass; d=google.com; s=arc-20160816; b=lQWEvbe7KAPjwAMlv9B4Q6NoAP/E60yV2WI+TDADgvakDaVvlhd1wdAsZHZq6rsYG6 q5dE2sm0s172ZSEuHZFxajxXI7nqTvYKiZ1et/cG0B08eNnZVxc/9sHEq4wk3V+UqjLf 4uP4TWjStdFeM0zPpAaq5On1RErdT23adfMTK5OBLcS84wV83croMhONiQ7Uf9C1MqW3 kUCzDCnWGJLmJpi4UGqfk0OTiFqKSn+PbnF+LI7zIpJ9fkQfIN0sFwoAC69cq0fwLojB uIzSju+idDPPGX8u03IrKyJ7Nd4MxNH0TGpYHeAdKt2m8fH5jdw0A1DG+9GRLhZqe2Y6 ahNw== 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=etkIGPMhez876ZbRfl7DUYJhAJblf65OK44K1ExmarE=; b=O3uFTRuBt0OyTMVU7rQpRVYb5JMdh4QJVE9hSm4HgMY1ug/fnbzhKg8Q9Cz7669o6c G4lvFmNDacOzFHKSn0ok7i4fCfuliYoidUWmcfTfrpNrv2QuKEbNUG+nSxL7yPdnmghJ 0UmqwgwBKKT1I2S93w5EBjJTsqKf/xzTEg9I4vyWeKVWz6IAKumFffzqsUjlCRsyw/Mm wbvV2BusE1mPkN3oeX3YuAdf3EOhj9DfFWw4rp2YWY+DfMBtnQhv2Er3wb8+ldd6+OJp LCeF9WtqHe1Bv7PusB8ZfCuMe7k4LWUuOgH+ahUJ5+YP8/cRtAKjZO2yoMyczW7oQZSY U5LQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=IZ7Lr183; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::329 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=etkIGPMhez876ZbRfl7DUYJhAJblf65OK44K1ExmarE=; b=Gbu/Q77eyBXp8XZ3eI6CRqp3amtcnbXbzXv1lzE7igRWyFR23Z85WxlVAdvPfaRo4+ 9X0uWWy0/GGL6DlzNbCHFaVIH+a/s87d4vDw12mMz+QG0bha0+SFA7IHQ1ETUbssH4E9 3gFHAKwSjHd1UKxlEdf1oS/TVxtM4UCZrg21aTzWvSWznw9mu0Z6Q/UseG6FAlfZaxrh hcS923XkSF6+JeUW1qTfqHDqkkZtmJgWIJ3h2BOn5Y4aSzCPaQs4VxmFNXhnHgyYBLjo caDIGn9t1DpuV6hyr6ra65dE32lLbIVa2sF/Y5Ja4kq7oTKC5tdLL8PtkMBBsjwc7HNy f89g== 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=etkIGPMhez876ZbRfl7DUYJhAJblf65OK44K1ExmarE=; b=R4+A6ms5K6EpfD6ocQd74QYJVEWchotN15dDK4TsR259sgvOtdy/TNQXbMl5h0AIhI 4HEDKnv8KTDnriiTMmHXpiOoWsP0UB4uP8+VUrEJm4nkH8jYrFY6ef5pVvM6pCh3E2Sj n3MMqWDHaLd0mI2blG0CrUr0gQD5fu9d5dL/l8ftQmXZleGLNGa13aHHdjFGUjdYJ0x6 JYPdZcbo7TNGGOBb+9F2DLleu61vdayutuocpQwQ80cjsgYCWrISnUOqebJ5KEv7KDdt a9+6NmQqDaii4EprbquNWlmZRMpqaSipivkuvcV8quAbAOcNdZPiWmM9BgbwUBrrAKoc sB3w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUP1iM7NxuTZag914RHj4xK/Qh0qX0K5NyNvAKjvs0Vr1Yglsim Te0DJGEHlog98HMRdNqglVQ= X-Google-Smtp-Source: APXvYqwNRbiKX2+WEPPvNqTwA/G2UZn+EncVs6JdIuHHk86AwwRGaMpXiJqBcfwrMQjrKVqfNdLGPw== X-Received: by 2002:ab0:13e6:: with SMTP id n35mr701116uae.90.1574806729026; Tue, 26 Nov 2019 14:18:49 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ab0:30d8:: with SMTP id c24ls164301uam.1.gmail; Tue, 26 Nov 2019 14:18:48 -0800 (PST) X-Received: by 2002:ab0:65d6:: with SMTP id n22mr672586uaq.132.1574806728435; Tue, 26 Nov 2019 14:18:48 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1574806728; cv=none; d=google.com; s=arc-20160816; b=NU8j3nJTmWEMc6PviOyMACm5NuxEn1LAzDD3NWOM6BP6uGbhuJHvce9ACHc2HNpvDm AXhkRt+XOs07x9PkuN+FtCXYpf0M8n8un1iyPOt4u85z00RLuf+79d6rCPefWbYKYm97 wNecfaGKPyZbepm6YhSl6D5jePUfUTHu+VS4f0YaUgof3cMNUxdFoRZb5+sLMrBkPjLK IyMnRjHDw72ZYLdL3WJw2c8Ym0qeoHap1yKshDpNUrFXWQn2Da2Vol6ljWQsxU0pGUox sI8LUvNPdEFssQIm0ug+jeylLPNiMtVLAwj5l+hQVxKhGv/eHAuYhZ3aWd3Q/TUTcjhK oE0w== 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=hydCZCJ1s/EKitQD/mkg7Jp+KLntgORq1xqQ2QjYA4k=; b=pWht4H9rcQ+73XeN9wFVxr6LPVHlBq/GywacfcS48FO0ro63L9Elm0eUJrA1xd5fQJ FPah6AT+G/MrAb7c9f9+0eOK9XXA4LZNFCTTHrAyHEjXK+NgoIyEqXqdDrxjHyRYr1qM uy9Kb+5bFPwYbc8+rK12RDl3lBL5pEfltBm0qHT98ivflLHWmbHRZ7QomIFul+n9O43R oVjp9xOLOTLwS+wWVmR+zsHPHNgRWdUH9m/kiVlZEi73KDESxSiiyjJ3B2k5YKQgqBAa VD9lBqggzViF5DFdnO0w5cm4O42Lq0m+F+R5imwGpfnPSHQQ2OGRD+ig3iwlJ5Ud6EBv 4D8w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=IZ7Lr183; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::329 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-ot1-x329.google.com (mail-ot1-x329.google.com. [2607:f8b0:4864:20::329]) by gmr-mx.google.com with ESMTPS id h143si436615vkh.1.2019.11.26.14.18.48 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 26 Nov 2019 14:18:48 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::329 as permitted sender) client-ip=2607:f8b0:4864:20::329; Received: by mail-ot1-x329.google.com with SMTP id w24so17393573otk.6 for ; Tue, 26 Nov 2019 14:18:48 -0800 (PST) X-Received: by 2002:a9d:58c8:: with SMTP id s8mr968016oth.27.1574806727718; Tue, 26 Nov 2019 14:18:47 -0800 (PST) Received: from mail-ot1-f48.google.com (mail-ot1-f48.google.com. [209.85.210.48]) by smtp.gmail.com with ESMTPSA id z4sm4049990ota.67.2019.11.26.14.18.46 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 26 Nov 2019 14:18:46 -0800 (PST) Received: by mail-ot1-f48.google.com with SMTP id z25so17370910oti.5 for ; Tue, 26 Nov 2019 14:18:46 -0800 (PST) X-Received: by 2002:a05:6830:1583:: with SMTP id i3mr961951otr.221.1574806725982; Tue, 26 Nov 2019 14:18:45 -0800 (PST) MIME-Version: 1.0 References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> <13f496d9-1d01-4a2f-b5c1-826dd87aebf2@googlegroups.com> In-Reply-To: From: Michael Shulman Date: Tue, 26 Nov 2019 14:18:34 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? To: Kevin Buzzard Cc: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , 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=IZ7Lr183; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::329 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: , Personally, I'm doubtful that one can ascribe any precise meaning to "canonical isomorphism", and therefore doubtful that one will be able to implement a computer proof assistant that can distinguish a "canonical isomorphism" from an arbitrary one. It's certainly worth thinking about, but my personal opinion is that instead of designing a proof assistant to match the way mathematicians think about "canonical isomorphisms", mathematicians are going to need to change the way they think. But it's just a question of going all the way down a road that they've already taken one step along. In formal systems like ZFC and Lean, almost no isomorphisms are equalities. Being willing to treat "canonical" isomorphisms as equalities is a first step into the brave new world of homotopy theory and higher category theory, but it's hard to find a place to stand when you've only taken that one step. In trying to make things precise, I think one feels inexorably pulled to the more consistent, and formalizable, position that *all* isomorphisms should be treated as equalities. It's not the same notion of equality, as Martin says, but it's a better replacement for it, which in particular can do everything that the old notion of equality could do when used "correctly" (e.g. equality of numbers and functions). On Tue, Nov 26, 2019 at 11:53 AM Kevin Buzzard wrote: > > Nicolas originally asked > > "So, to put this into one concrete question, how (if at all) is HoTT-Coq > more practical than Mizar for the purpose of formalizing mathematics, > outside the specific realm of synthetic homotopy theory?" > > One issue with this question is that different people mean different thin= gs by "mathematics". As someone who was until recently an outsider to forma= lising but very much a "working mathematician", I think I've made it pretty= clear on this forum and others that for the majority of people in e.g. my = maths department, they would say that none of the systems have really got a= nywhere concerning modern day mathematics, which is the kind of mathematics= that the majority of mathematicians working in maths departments are inter= ested in. This is a dismal state of affairs and one which I would love to h= elp change, but it needs a cultural change within mathematics departments. = The Mizar stuff I've seen has mostly been undergraduate level mathematics. = UniMath seems to be a massive amount of category theory and not much underg= raduate level mathematics at all. On the other hand, "there is a lot more c= ategory theory in the HoTT systems than in Mizar, so maybe Hott-Coq is more= practical than Mizar for category theory" might be an answer to the origin= al question. > > I'm interested in algebraic geometry, and in algebraic geometry there is = this convention (explicitly flagged in Milne's book on etale cohomology) th= at the notation for "canonical isomorphism" (whatever that means) is "=3D".= One can call this "mathematical equality" and it comes with a warning that= it is not well-defined. I think one reason it's a challenge to formalise m= odern algebraic geometry is that none of the systems seem to have this kind= of equality (perhaps because all of the systems demand well-defined defini= tions!). What I meant by my earlier post was that the `=3D` I have run into= in Lean's type theory is too weak (canonically isomorphic things can't be = proved to be equal) but the one I have run into in HoTT seems too strong (n= on-canonically isomorphic things are equal). > > It would not surprise me if different areas of mathematics had different = concepts of equality. Mathematicians seem to use the concept very fluidly. = Maybe it is the case that the areas where "mathematical equality" is closer= to e.g. Lean's `=3D` or Mizar's `=3D` or UniMath's `=3D` or Isabelle/HOL's= `=3D` or whatever, will find that formalising goes more easily in Lean's t= ype theory/Mizar/HoTT/HOL or whatever. The biggest problem with this conjec= ture is that equality is mostly a cut-and-dried thing at undergraduate leve= l, and there is not enough harder maths formalised in any of these systems = (obviously there are several monumental theorems but I'm dreaming about far= greater things) for us to start to check. Note that people like Riemann ha= d no idea about set theory but did a lot of complex analysis, and he really= only needed to worry about equality of complex numbers and equality of fun= ctions from the complexes to the complexes, so I don't think it's a coincid= ence that a whole bunch of complex analysis is done in Isabelle/HOL, which = seems to me to be the "simplest logic" of the lot. Probably all the systems= model this equality well. > > Kevin > > > On Tue, 26 Nov 2019 at 19:14, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: >> >> >> >> On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: >>> >>> HoTT instead expands the notion of "equality" to >>> essentially mean "isomorphism" and requires transporting along it as a >>> nontrivial action. I doubt that that's what you have in mind, but >>> maybe you could explain what you do mean? >> >> >> I think terminology and notation alone cause a lot of confusion (and I >> have said this many times in this list in the past, before Kevin joined = in). >> >> Much of the disagreement is not a real disagreement but a >> misunderstanding. >> >> * In HoTT, or in univalent mathematics, we use the terminology >> "equals" and the notation "=3D" for something that is not the same >> notion as in "traditional mathematics". >> >> * Before the univalence axiom, we had Martin-Loef's identity type. >> >> * It was *intended* to capture equality *as used by mathematicians* >> (constructive or not). >> >> * But it didn't. Hofmann and Streicher proved that. >> >> * The identity type captures something else. >> >> It certainly doesn't capture truth-valued equality by default. >> >> In particular, Voevosdky showed that it captures isomorphism of >> sets, and more generality equivalence of =E2=88=9E-groupoids. >> >> But this is distorting history a bit. >> >> In the initial drafts of his "homotopy lambda calculus", he tried >> come up with a new construction in type theory to capture >> equivalence. >> >> It was only later that he found out that what he needed was >> precisely Martin-Loef's identity type. >> >> * So writing "x =3D y" for the identity type is a bit perverse. >> >> People may say, and they have said "but there is no other sensible >> notion of equality for such type theories. >> >> That may be so, but because, in any case, *it is not the same >> notion of equality*, we should not use the same symbol. >> >> * Similarly, writing "X =E2=89=83 Y" is a bit perverse, too. >> >> In truth-valued mathematics, "X =E2=89=83 Y" is most of the time inte= nded >> to be truth-valued, not set-valued. >> >> (Exception: category theory. E.g. we write a long chain of >> isomorphisms to establish that two objects are isomorphic. Then we >> learn that the author of such a proof was not interested in the >> existence of an isomorphism, but instead to provide an >> example. Such a proof/construction is usually concluded by saying >> something like "by chasing the isomorphism, we see that we can take >> [...] as our desired isomorphism.) >> >> >> * With the above out of the way, we can consider the imprecise slogan >> "isomorphic types are equal". >> >> The one thing that the univalence axiom doesn't say is that >> isomorphic type are equal. >> >> What it does say is that the *identity type* Id X Y is in canonical >> bijection with the type X =E2=89=83 Y of equivalences. >> >> * What is the effect of this? >> >> - That the identity type behaves like isomorphism, rather than like >> equality. >> >> - And that isomorphism behaves a little bit like equality. >> >> The important thing above is "a little bit". >> >> In particular, we cannot *substitute* things by isomorphic >> things. We can only *transport* them (just like things work as >> usual with isomorphisms). >> >> * Usually, the univalence axioms is expressed as a relation between >> equality and isomorphism. >> >> Where by equality we don't mean equality but instead the identity >> type. >> >> A way to avoid these terminological problems is to formulate >> univalence as a property of isomorphisms, or more precisely >> equivalences. >> >> To show that all equivalences satisfy a given property, it is >> enough to prove that all the identity equivalence between any two >> types have this property. >> >> * So, as Mike says above, most of the time we can work with type >> equivalence rather than "type equality". And I do too. >> >> Something that is not well explained at all in the literature is >> when and how the univalence axiom *actually makes a difference*. >> >> (I guess this is not well understood. I used to thing that the >> univalence axioms makes a difference only for types that are not >> sets. But actually, for example, the univalence axiom is needed (in >> the absence of the K axiom) to prove that the type of ordinals is a >> set.) >> >> * One example: object classifiers, subtype classifiers, ... >> >> * Sometimes the univalence axiom may be *convenient* but *not needed*. >> >> I guess that Kevin is, in particular, saying precisely that. In all >> cases where he needs to transport constructions along isomorphisms, >> he is confident that this can be done without univalence. And I >> would agree with this assessment. >> >> Best, >> Martin >> >> >> >> >> -- >> 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. >> To view this discussion on the web visit https://groups.google.com/d/msg= id/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.c= om. > > -- > 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/msgi= d/HomotopyTypeTheory/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84aTxLT0kwd5syASy31Aw%40= mail.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/CAOvivQyAaJnLeJZHCMqWAu3f%2BOb72%2BMSSLmb8MjkBHoH05k_Rw%= 40mail.gmail.com.