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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wr1-x437.google.com (mail-wr1-x437.google.com [IPv6:2a00:1450:4864:20::437]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 648259a6 for ; Tue, 26 Nov 2019 19:53:20 +0000 (UTC) Received: by mail-wr1-x437.google.com with SMTP id c12sf9738870wrq.7 for ; Tue, 26 Nov 2019 11:53:20 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1574797999; cv=pass; d=google.com; s=arc-20160816; b=Uqv3LT3q6JGFBUWJjsKMf/KFRuHE7xUmoNuhB+iBHX2IwWwlEP2TUlPStf37KHk5oZ bjBWyMcA4EZnNNPvkAZNWRuV0a3rHyFO18fFBigfudW4GsoR2xkyVrcjvv3WshLAE9gr vDMIZe/tpb6f2Juth/wXiaZiohSgCn7WWWF4CaNnc+utzHmS/GgrC0lTgmvI355PLqYB YyeH/C3RwodT7BBhRs1WYtiv8Q+kbUScx6GC/MUy0sdl4np6/wf6eM24FriXK/T+namb idWlsnTBhiG/msGTcXEKvoaEQCs6hRwOtxY7nQyTs2qvCfPU7T5SCaaOKMLgmC3u5lJg cmPA== 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 :dkim-signature; bh=xDSSuRm8o2jvC4kdO8GyOtSmiYDS4dagDcklFLcaVzs=; b=rq7DjlufvomOvg5zg2n0ZHugRgOALEFp6D9UT7YO5UE7360O3/L+m1VYV779/4Q2kG /D43HAOQdQzffq8yhxQBFk37H3HkRKIlRwnXfSVvGVA1BRDIyAD1s6Xc+A4I84sJeO++ Aqa0VaNQ4cuA4Zypwl7NX9WzwKPguAXT81MU5deqaLr3jm4QwhMjV697eMM4wxAz7scI SkNo87enVyMbxSe0C07h7XC8/pJO/C7cKgOPwVa73pHm9YT//Sny/F6u15SbHeO8JFPk Z7ne37Rex1X5yR9j/BL4P6aJxJ0XE7ldPDdBbRafD/SqtCo8/mJO023FuzJlNtEAvcFe BDdw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=jgPHhnGI; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22c as permitted sender) smtp.mailfrom=kevin.m.buzzard@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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=xDSSuRm8o2jvC4kdO8GyOtSmiYDS4dagDcklFLcaVzs=; b=V+6WG1LfnNUTdZV6nU9ydjJELN/Qs6Om3dqOQ//53OXd4qu8ICbBkQhGNcTDOs419r nAK0Uc+VI9xoGjrOCh021tnVEt8lRSl94XLCy6vUywzU/42MmLBkJP2Y+IAZPhjYvQjz loObhIBeUJXvo5CLBT1GyseofI4Be1CokigEWG+pCu03s6ipXXLAn5CKDs6zuOh15Rn+ pfXfccjbMT2mwp+3zZkZRuRlHNfzuoDv2tHHpoG+0EpNa2Jp/DRFKhbq9iVylHTBtCZQ 3wrGAcoW35e+ptYAK6OWrsEnDklS91jLFeiPlx6RVab8GTACtefN3ElraTZA9OasnIzx sjVA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=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=xDSSuRm8o2jvC4kdO8GyOtSmiYDS4dagDcklFLcaVzs=; b=TcP1D8V0tqYJugpqga5DWc35Bo7XpTQ5R9r3GlQxKxymoVQ+702YhrHxxVuEzQzLkV +1jOwKm+T4gv6ilocQZljBONI0PR57H5L/Mdl6/zvmqGWK0CT64RlHumtKB2IT3LCZz6 C6SLWotX7EhXnqceFwQv0VoodrjjDXCECYMDbhXH49sZ2HXN2rXKdcpYE80JHsMMRz6M Nbio+KtCJRGHF808bIvkeRoVoe9kfeihLwN07qRDuO0qy3hI5lp0iem46tK+WtoRf7XQ e7rbhCcpdfRni8ddQOQaXTd7N4rSur2Vxoa5Jsk/nfVOTT6j5NbBdfD3PR5FOGi9vtDD IAKA== 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=xDSSuRm8o2jvC4kdO8GyOtSmiYDS4dagDcklFLcaVzs=; b=DPJTB8HlnDENvHDIjVsp5hfH+AVm8N3pRrrMSJfE/UjBcIbnOA+3e4NIvoNxYmo6Z4 /b82k3EOQ/TI2BAeBPmYom7unGaRToVhpxThE8zoXpezxLhfkMwHpvZOyDedkGj4XUtU +fJ7b2M2dCtBsm2tjdqU8utsbhIz/ni2cNrxc0NL3Pf7wrh89DhICcbKbm5ERwextTh1 6r0zZlcxeI/VhqjXu9gnCrfsS4dEp6y/E9ILL0m4VOeIw3z+cuXSsZReMgBt79NylWUo i3slVJwnFVDfTraJYSfLU9XHYo7cSa3rjihayKM2gKM9h8DM5O5Udxkrn7SyAvVS6Mii q0oQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVf78rvmTQG5em0gshg61IZUErtbyhHSnHz4/pEXBdNM1ZgHK7W X36Mp6+S7llCZf8iN4mzxuc= X-Google-Smtp-Source: APXvYqzQUFkNeHamTLryoOkqPSv0zUVSiHZDBYTTB8WeqPTFZG3BLK4G1Ylp+Grdq0ONTJjcVYFQMw== X-Received: by 2002:a5d:55c7:: with SMTP id i7mr40055758wrw.64.1574797999059; Tue, 26 Nov 2019 11:53:19 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:6385:: with SMTP id x127ls382169wmb.2.gmail; Tue, 26 Nov 2019 11:53:18 -0800 (PST) X-Received: by 2002:a05:600c:34c:: with SMTP id u12mr747329wmd.3.1574797998291; Tue, 26 Nov 2019 11:53:18 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1574797998; cv=none; d=google.com; s=arc-20160816; b=cocT3jVDwNLDgj0rh20rYohYxMM78TeWH90cy39KPEVpoI1n2MRw7coJmb2qeMChpn R9kfNIZfrrqOE4qtvdC75vRwNYx78U9IcmZ5s3zi9w/AvOLnfaAf6jLcPCNEJsl/LUAR 3UagzlfkOeLVp6ye4oYJHHxS07rR6vi7AtPmlWysi2r5oQ2l2YQeBWDDBx6runI+Bt06 yyWN3yd9pVGOGYySefTg8DSR11gSC50o1/uyBKlIykJyLzEXTOrid9DVpYdNB7mBtiTv U4qAe3Fd7qJu/+dVflYC1YbJ2XIC2W2Z7wAbrfUMIROrvO/P2CldPHHQDkqo4Z/gtQsu S5XA== 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=yvHhdB8TzHTP8lljtGZ74Mn4jCPoHRfWKGz3D2hSn2A=; b=MRgA489NhM7v4sFEuIXzYrOCsmokpYIEaKphgfDiu/3W/8TMNO65zs8JS6cJtMqKC2 5mtzR/b4NYdQKgCi7dgg9+hFKep+9yysv4TDtZ//lFQqDaipFdnATHS8gk780uXcQd19 1sKm1K07LamJqBebmuslSvVEc8LbSZvtoIThSn7nz29Px/6zPI55G3rg8RMHSqTGRdlp PCAlaczpEo+ce+Eq15S+8OvNowy4PxGYwalT3r/zJXcB6j/6k6Zs3ynP6ooYPOAPNfNq p80A/I0zEpuZ/HaZr/AZjoqVGd8Fm/S9YFMWqoswj+4f7FONLKPXZEWAnXTS6RnUmEcL G+AQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=jgPHhnGI; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22c as permitted sender) smtp.mailfrom=kevin.m.buzzard@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lj1-x22c.google.com (mail-lj1-x22c.google.com. [2a00:1450:4864:20::22c]) by gmr-mx.google.com with ESMTPS id r11si597224wrl.3.2019.11.26.11.53.18 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 26 Nov 2019 11:53:18 -0800 (PST) Received-SPF: pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22c as permitted sender) client-ip=2a00:1450:4864:20::22c; Received: by mail-lj1-x22c.google.com with SMTP id k8so11123797ljh.5 for ; Tue, 26 Nov 2019 11:53:18 -0800 (PST) X-Received: by 2002:a2e:9f4d:: with SMTP id v13mr28259660ljk.78.1574797997915; Tue, 26 Nov 2019 11:53:17 -0800 (PST) MIME-Version: 1.0 References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> <13f496d9-1d01-4a2f-b5c1-826dd87aebf2@googlegroups.com> In-Reply-To: <13f496d9-1d01-4a2f-b5c1-826dd87aebf2@googlegroups.com> From: Kevin Buzzard Date: Tue, 26 Nov 2019 19:53:00 +0000 Message-ID: Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000424df80598453b26" X-Original-Sender: kevin.m.buzzard@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=jgPHhnGI; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22c as permitted sender) smtp.mailfrom=kevin.m.buzzard@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --000000000000424df80598453b26 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 things by "mathematics". As someone who was until recently an outsider to formalising 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 anywhere concerning modern day mathematics, which is the kind of mathematics that the majority of mathematicians working in maths departments are interested in. This is a dismal state of affairs and one which I would love to help 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 undergraduate level mathematics at all. On the other hand, "there is a lot more category 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 original question. I'm interested in algebraic geometry, and in algebraic geometry there is this convention (explicitly flagged in Milne's book on etale cohomology) that 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 modern algebraic geometry is that none of the systems seem to have this kind of equality (perhaps because all of the systems demand well-defined definitions!). What I meant by my earlier post was that the `=3D` I have ru= n 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 (non-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 type theory/Mizar/HoTT/HOL or whatever. The biggest problem with this conjecture is that equality is mostly a cut-and-dried thing at undergraduate level, 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 had 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 functions from the complexes to the complexes, so I don't think it's a coincidence 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 < escardo.martin@gmail.com> 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 inten= ded > 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 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/13f496d9-1d01-4a2f-b= 5c1-826dd87aebf2%40googlegroups.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/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84aTxLT0kwd5syASy31Aw%40ma= il.gmail.com. --000000000000424df80598453b26 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Nicolas originally asked

&qu= ot;So, to put this into one concrete question, how (if at all) is HoTT-Coq<= br> 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 dif= ferent things by "mathematics". As someone who was until recently= an outsider to formalising but very much a "working mathematician&quo= t;, 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 no= ne of the systems have really got anywhere concerning modern day mathematic= s, which is the kind of mathematics that the majority of mathematicians wor= king in maths departments are interested in. This is a dismal state of affa= irs and one which I would love to help change, but it needs a cultural chan= ge 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 undergraduate level mathematics at all. On= the other hand, "there is a lot more category theory in the HoTT syst= ems than in Mizar, so maybe Hott-Coq is more practical than Mizar for categ= ory theory" might be an answer to the original question.
I'm interested in algebraic geometry, and in algebraic geom= etry there is this convention (explicitly flagged in Milne's book on et= ale cohomology) that the notation for "canonical isomorphism" (wh= atever 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 modern algebraic geometr= y is that none of the systems seem to have this kind of equality (perhaps b= ecause all of the systems demand well-defined definitions!). What I meant b= y my earlier post was that the `=3D` I have run into in Lean's type the= ory is too weak (canonically isomorphic things can't be proved to be eq= ual) but the one I have run into in HoTT seems too strong (non-canonically = isomorphic things are equal).

It would not su= rprise me if different areas of mathematics had different concepts of equal= ity. Mathematicians seem to use the concept very fluidly. Maybe it is the c= ase 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 type theory/Mizar/HoTT/HOL or whatever. The biggest problem wit= h this conjecture is that equality is mostly a cut-and-dried thing at under= graduate level, and there is not enough harder maths formalised in any of t= hese systems (obviously there are several monumental theorems but I'm d= reaming about far greater things) for us to start to check. Note that peopl= e like Riemann had no idea about set theory but did a lot of complex analys= is, and he really only needed to worry about equality of complex numbers an= d equality of functions from the complexes to the complexes, so I don't= think it's a coincidence that a whole bunch of complex analysis is don= e in Isabelle/HOL, which seems to me to be the "simplest logic" o= f the lot. Probably all the systems model this equality well.
Kevin


On Tue, 26 Nov 2019 at 19:14, Mar= t=C3=ADn H=C3=B6tzel Escard=C3=B3 <escardo.martin@gmail.com> wrote:


On Tuesday, 26 No= vember 2019 00:25:37 UTC, Michael Shulman wrote:
HoTT instead expands the notion of "equality&q= uot; to
essentially mean "isomorphism" and requires transporting alon= g it as a
nontrivial action.=C2=A0 I doubt that that's what you have in mind,= but
maybe you could explain what you do mean?

=C2=A0I 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
misund= erstanding.

=C2=A0* In HoTT, or in univalent mathe= matics, we use the terminology
=C2=A0 =C2=A0"equals" an= d the notation "=3D" for something that is not the same
=C2=A0 =C2=A0notion as in "traditional mathematics".
<= br>
=C2=A0* Before the univalence axiom, we had Martin-Loef's= identity type.

=C2=A0* It was *intended* to captu= re equality *as used by mathematicians*
=C2=A0 =C2=A0(constructiv= e or not).

=C2=A0* But it didn't. Hofmann and = Streicher proved that.

=C2=A0* The identity type c= aptures something else.

=C2=A0 =C2=A0It certainly = doesn't capture truth-valued equality by default.

<= div>=C2=A0 =C2=A0In particular, Voevosdky showed that it captures isomorphi= sm of
=C2=A0 =C2=A0sets, and more generality equivalence of =E2= =88=9E-groupoids.

=C2=A0 =C2=A0But this is distort= ing history a bit.

=C2=A0 =C2=A0In the initial dra= fts of his "homotopy lambda calculus", he tried
=C2=A0 = =C2=A0come up with a new construction in type theory to capture
= =C2=A0 =C2=A0equivalence.

=C2=A0 =C2=A0It was only= later that he found out that what he needed was
=C2=A0 =C2=A0pre= cisely Martin-Loef's identity type.

=C2=A0* So= writing "x =3D y" for the identity type is a bit perverse.
=

=C2=A0 =C2=A0People may say, and they have said "b= ut there is no other sensible
=C2=A0 =C2=A0notion of equality for= such type theories.

=C2=A0 =C2=A0That may be so, = but because, in any case, *it is not the same
=C2=A0 =C2=A0notion= of equality*, we should not use the same symbol.

= =C2=A0* Similarly, writing "X =E2=89=83 Y" is a bit perverse, too= .

=C2=A0 =C2=A0In truth-valued mathematics, "= X =E2=89=83 Y" is most of the time intended
=C2=A0 =C2=A0to = be truth-valued, not set-valued.

=C2=A0 =C2=A0(Exc= eption: category theory. E.g. we write a long chain of
=C2=A0 =C2= =A0isomorphisms to establish that two objects are isomorphic. Then we
=
=C2=A0 =C2=A0learn that the author of such a proof was not interested = in the
=C2=A0 =C2=A0existence of an isomorphism, but instead to p= rovide an
=C2=A0 =C2=A0example. Such a proof/construction is usua= lly concluded by saying
=C2=A0 =C2=A0something like "by chas= ing the isomorphism, we see that we can take
=C2=A0 =C2=A0[...] a= s our desired isomorphism.)


=C2=A0*= With the above out of the way, we can consider the imprecise slogan
<= div>=C2=A0 =C2=A0"isomorphic types are equal".

=C2=A0 =C2=A0The one thing that the univalence axiom doesn't say= is that
=C2=A0 =C2=A0isomorphic type are equal.

=C2=A0 =C2=A0What it does say is that the *identity type* Id X Y i= s in canonical
=C2=A0 =C2=A0bijection with the type X =E2=89=83 Y= of equivalences.

=C2=A0* What is the effect of th= is?

=C2=A0 =C2=A0- That the identity type behaves = like isomorphism, rather than like
=C2=A0 =C2=A0 =C2=A0equality.<= /div>

=C2=A0 =C2=A0- And that isomorphism behaves a litt= le bit like equality.

=C2=A0 =C2=A0The important t= hing above is "a little bit".

=C2=A0 =C2= =A0In particular, we cannot *substitute* things by isomorphic
=C2= =A0 =C2=A0things. We can only *transport* them (just like things work as
=C2=A0 =C2=A0usual with isomorphisms).

=C2= =A0* Usually, the univalence axioms is expressed as a relation between
=C2=A0 =C2=A0equality and isomorphism.

=C2= =A0 =C2=A0Where by equality we don't mean equality but instead the iden= tity
=C2=A0 =C2=A0type.

=C2=A0 =C2=A0A w= ay to avoid these terminological problems is to formulate
=C2=A0 = =C2=A0univalence as a property of isomorphisms, or more precisely
=C2=A0 =C2=A0equivalences.

=C2=A0 =C2=A0To show t= hat all equivalences satisfy a given property, it is
=C2=A0 =C2= =A0enough to prove that all the identity equivalence between any two
<= div>=C2=A0 =C2=A0types have this property.

=C2=A0*= So, as Mike says above, most of the time we can work with type
= =C2=A0 =C2=A0equivalence rather than "type equality". And I do to= o.

=C2=A0 =C2=A0Something that is not well explain= ed at all in the literature is
=C2=A0 =C2=A0when and how the univ= alence axiom *actually makes a difference*.

=C2=A0= =C2=A0(I guess this is not well understood. I used to thing that the
=
=C2=A0 =C2=A0univalence axioms makes a difference only for types that = are not
=C2=A0 =C2=A0sets. But actually, for example, the univale= nce axiom is needed (in
=C2=A0 =C2=A0the absence of the K axiom) = to prove that the type of ordinals is a
=C2=A0 =C2=A0set.)
<= div>
=C2=A0 =C2=A0 =C2=A0 * One example: object classifiers, = subtype classifiers, ...

=C2=A0* Sometimes the uni= valence axiom may be *convenient* but *not needed*.

=C2=A0 =C2=A0I guess that Kevin is, in particular, saying precisely that.= In all
=C2=A0 =C2=A0cases where he needs to transport constructi= ons along isomorphisms,
=C2=A0 =C2=A0he is confident that this ca= n be done without univalence. And I
=C2=A0 =C2=A0would agree with= this assessment.

Best,
Martin


=C2=A0

--
You received this message because you are subscribed to the Google Groups &= quot;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 ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-= 826dd87aebf2%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups &= quot;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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84a= TxLT0kwd5syASy31Aw%40mail.gmail.com.
--000000000000424df80598453b26--