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=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-oi1-x23f.google.com (mail-oi1-x23f.google.com [IPv6:2607:f8b0:4864:20::23f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a0a019c0 for ; Sun, 3 Nov 2019 22:23:28 +0000 (UTC) Received: by mail-oi1-x23f.google.com with SMTP id v205sf964820oig.7 for ; Sun, 03 Nov 2019 14:23:28 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=+VirwE2bC+z/BfWq2XwhWkeovsodXuAbeteePgRo6ek=; b=UOeeHWp++0J+hOel2Nvrg26ZGvtZLXLCUZsLnJDgc+j14k8polISXsRNlE5d4j2GbE LO47wbg8XJTAzDYpT+Bi7aweKYuKwHvItyuoXY+a07Dc1ZsUbW5/u3p3/OPb769+Gl8c 45V5fKr9IOJz1GgosBDy1Dq9RH/Aiz1Ui6BSZgc5Uxb71oWehzkRYNGE+rqDm+1V1YgH jjGieyVbOU9pEqFclFDwFLO2gYuQZzP9aHmH8ZF9LwoN0e2Dj9T76Uxz9L5gHJI0ltsF BMKZJ3d8TJYJWd/IFGElawSKSE+VWnfovQx7yU2z3uBvsynWFPn1Mb1pPEsWc8SzGOl/ Txag== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=+VirwE2bC+z/BfWq2XwhWkeovsodXuAbeteePgRo6ek=; b=r7/rzbTArNU6+3hRW+Zo3CCPpFE4stBnLa+s+CaykjRT95uw8zs4kvlRgNfDFvLByF hnYes3m76micvUKhOlqI8kK5DzLFOSGWfuPUffvopow27ydxNDwqmE579NUyX30kIssz SQRHWzZxlop/gnYM0GmHd5RT7YkLmnGRkXzhMGBnvA07GQXW/ZwTAHTGkwuoLnJy8kLW I1RhGcxeWuZ2U5nxV5AW3dbPBBj8JFSiHwJeSsrBYmlEDSV8tKYxIjHjKT8mIoVgX+GU O1WIQU0ue/XSnKvJO9N0GAZplLuyQPbgZfwXULlTjR81yAPp7BF1RwotRFQGa89WUFdd 3amg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=+VirwE2bC+z/BfWq2XwhWkeovsodXuAbeteePgRo6ek=; b=LtwyK5BGZC9MzmIvJDDCYWlI7edvvvFRfVWAkciq9dbMg8I1ungIOMd5xFfxR7CXh5 ncl02M5Y80JcTvGpSijc0lEMACad/AkLM7RvIBTAbOEiNpKmXF6Cln9sv5BqcO2jR87i j6M9N7ris40/olWd+aurL2unTtR5VQjkPrcjAWUTyGZYs1AUynFByjKHKGLeZDPcf1+e EG7TlRthekbo1aYgRltdWQ0X+ug2YG3GAiJJwtH45XIXAEzH725S6udXEIWLuEy/pAKE s8vIPgCHJX2Jiu53ZqNyqwQUTJFa3aRLZXKts4/qUvxQTWG1C8npT40Jwh+8LOW/xZ49 WHQw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUncy7t31Np0T1uxGptlIg7kR8uAzUNBP7ndprB9AIRU/e7thpM psPBojFVWgbzaX9n9V9n43w= X-Google-Smtp-Source: APXvYqw7tCLBEGfMGfXuLPUPOUd1nSYe1nBMLixUmxXIH4/iOwJL2WKr3Uk7CRzFUHqyYPh5Nxw/Mw== X-Received: by 2002:a9d:5e1a:: with SMTP id d26mr15694159oti.96.1572819806938; Sun, 03 Nov 2019 14:23:26 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6830:1f4a:: with SMTP id u10ls1603520oth.9.gmail; Sun, 03 Nov 2019 14:23:26 -0800 (PST) X-Received: by 2002:a05:6830:55a:: with SMTP id l26mr8605526otb.144.1572819805857; Sun, 03 Nov 2019 14:23:25 -0800 (PST) Date: Sun, 3 Nov 2019 14:23:25 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> In-Reply-To: References: Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_962_393102267.1572819805225" X-Original-Sender: escardo.martin@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: , ------=_Part_962_393102267.1572819805225 Content-Type: multipart/alternative; boundary="----=_Part_963_1059132255.1572819805226" ------=_Part_963_1059132255.1572819805226 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable This discussion reminds me of this=20 question: https://mathoverflow.net/questions/336191/cauchy-reals-and-dedeki= nd-reals-satisfy-the-same-mathematical-theorems/336233?noredirect=3D1#comme= nt840649_336233 M. On Sunday, 3 November 2019 19:46:32 UTC, Valery Isaev wrote: > > The isomorphism invariance might be useful when you don't care about the= =20 > actual stuff you get after transporting. If you have two different=20 > definitions of the same set, you can transport its *properties* along the= =20 > isomorphism (that you still need to construct). For example, we can defin= e=20 > rational numbers in two different ways: as arbitrary quotients and as=20 > reduced quotients. Then you can prove that they are isomorphic and that o= ne=20 > of them gives you a field. Then you know that the other one is also a=20 > field. You may be interested in the actual definitions of the operations,= =20 > but you dob't usually care about the actual proof of the properties. So,= =20 > you construct the addition and the multiplication explicitly, but you get= =20 > proofs that they determine a field "for free" from the other definition. = If=20 > the proofs for one of the definitions is easier than for the other one,= =20 > this might be a significant simplification. > > Regards, > Valery Isaev > > > =D0=B2=D1=81, 3 =D0=BD=D0=BE=D1=8F=D0=B1. 2019 =D0=B3. =D0=B2 22:13, Mich= ael Shulman >: > >> But does univalence a la Book HoTT *actually* make it easier to reason >> about such things? It allows us to write "=3D" rather than "\cong", but >> to construct such an equality we have to construct an isomorphism >> first, and to *use* such an equality we have to transport along it, >> and then we get lots of univalence-redexes that we have to manually >> reduce away. My experience formalizing math in HoTT/Coq is that it's >> much easier if you *avoid* turning equivalences into equalities except >> when absolutely necessary. (I don't have any experience formalizing >> math in a cubical proof assistant, but in that case at least you >> wouldn't have to manually reduce the univalence-redexes -- although it >> seems to me you'd still have to construct the isomorphism before you >> can apply univalence to make it an equality.) >> >> On Sun, Nov 3, 2019 at 3:57 AM David Roberts > > wrote: >> > >> > Forget even higher category theory. Kevin Buzzard now goes around=20 >> telling the story of how even formally proving (using Lean) things in=20 >> rather elementary commutative algebra from EGA that are stated as=20 >> equalities was not obvious: the equality is really an isomorphism arisin= g=20 >> from a universal property. Forget trying to do anything motivic, when=20 >> algebra is full of such equalities. This is not a problem with univalenc= e,=20 >> of course. >> > >> > David >> > >> > On Sun, 3 Nov 2019, 10:08 PM Bas Spitters > > wrote: >> >> >> >> There's also VV homotopy lambda calculus, which he later abandoned fo= r=20 >> MLTT: >> >>=20 >> https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hla= mbda_short_current.pdf >> >> >> >> On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters > > wrote: >> >>> >> >>> I believe it refers to his 2-theories: >> >>> https://www.ias.edu/ideas/2014/voevodsky-origins >> >>> >> >>> On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt < >> ze...@fromzerotoinfinity.xyz > wrote: >> >>>> >> >>>> In [this](https://www.youtube.com/watch?v=3Dzw6NcwME7yI&t=3D1680) 2= 014=20 >> talk >> >>>> at IAS, Voevodsky talks about the history of his project of=20 >> "univalent >> >>>> mathematics" and his motivation for starting it. Namely, he mention= s >> >>>> that he found existing proof assistants at that time (in 2000) to b= e >> >>>> impractical for the kinds of mathematics he was interested in. >> >>>> >> >>>> Unfortunately, he doesn't go into details of what mathematics he wa= s >> >>>> exactly interested in (I'm guessing something to do with homotopy >> >>>> theory) or why exactly existing proof assistants weren't practical= =20 >> for >> >>>> formalizing them. Judging by the things he mentions in his talk, it >> >>>> seems that (roughly) his rejection of those proof assistants was=20 >> based >> >>>> on the view that predicate logic + ZFC is not expressive enough. In >> >>>> other words, there is too much lossy encoding needed in order to >> >>>> translate from the platonic world of mathematical ideas to this=20 >> formal >> >>>> language. >> >>>> >> >>>> Comparing the situation to computer programming languages, one migh= t=20 >> say >> >>>> that predicate logic is like Assembly in that even though everythin= g=20 >> can >> >>>> be encoded in that language, it is not expressive enough to directl= y >> >>>> talk about higher level concepts, diminishing its practical value f= or >> >>>> reasoning about mathematics. In particular, those systems are not >> >>>> adequate for *interactive* development of *new* mathematics (as=20 >> opposed >> >>>> to formalization of existing theories). >> >>>> >> >>>> Perhaps I am just misinterpreting what Voevodsky said. In this case= ,=20 >> I >> >>>> hope someone can correct me. However even if this wasn't *his* view= ,=20 >> to >> >>>> me it seems to be a view held implicitly in the HoTT community. In= =20 >> any >> >>>> case, it's a view that one might reasonably hold. >> >>>> >> >>>> However I wonder how reasonable that view actually is, i.e. whether= =20 >> e.g. >> >>>> Mizar really is that much more impractical than HoTT-Coq or Agda,= =20 >> given >> >>>> that people have been happily formalizing mathematics in it for 46= =20 >> years >> >>>> now. And, even though by browsing the contents of "Formalized >> >>>> Mathematics" one can get the impression that the work consists=20 >> mostly of >> >>>> formalizing early 20th century mathematics, neither the UniMath nor= =20 >> the >> >>>> HoTT library for example contain a proof of Fubini's theorem. >> >>>> >> >>>> So, to put this into one concrete question, how (if at all) is=20 >> HoTT-Coq >> >>>> more practical than Mizar for the purpose of formalizing mathematic= s, >> >>>> outside the specific realm of synthetic homotopy theory? >> >>>> >> >>>> >> >>>> -- >> >>>> >> >>>> Nicolas >> >>>> >> >>>> >> >>>> -- >> >>>> You received this message because you are subscribed to the Google= =20 >> Groups "Homotopy Type Theory" group. >> >>>> To unsubscribe from this group and stop receiving emails from it,= =20 >> send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com=20 >> . >> >>>> To view this discussion on the web visit=20 >> https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-= dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz >> . >> >> >> >> -- >> >> You received this message because you are subscribed to the Google=20 >> Groups "Homotopy Type Theory" group. >> >> To unsubscribe from this group and stop receiving emails from it, sen= d=20 >> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com >> . >> >> To view this discussion on the web visit=20 >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAb= B%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com >> . >> > >> > -- >> > You received this message because you are subscribed to the Google=20 >> Groups "Homotopy Type Theory" group. >> > To unsubscribe from this group and stop receiving emails from it, send= =20 >> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com >> . >> > To view this discussion on the web visit=20 >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS= 16Vy7sGiEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.com >> . >> >> --=20 >> You received this message because you are subscribed to the Google Group= s=20 >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n=20 >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com . >> To view this discussion on the web visit=20 >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQz47kSm9WbKDm= UsndrpAJMkNwiWmVABqOFrVqyTOvSAbw%40mail.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/2ca6c47c-6196-4b45-b82c-db79b2b6568c%40googlegroups.com. ------=_Part_963_1059132255.1572819805226 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
This discussion reminds me of this question:=C2=A0https://= mathoverflow.net/questions/336191/cauchy-reals-and-dedekind-reals-satisfy-t= he-same-mathematical-theorems/336233?noredirect=3D1#comment840649_336233
M.

On Sunday, 3 November 2019 19:46:32 UTC, Valery = Isaev wrote:
=
The isomorphism invariance might be useful when you don't care abo= ut the actual stuff you get after transporting. If you have two different d= efinitions of the same set, you can transport its properties=C2=A0al= ong the isomorphism (that you still need to construct). For example, we can= define rational numbers in two different=C2=A0ways: as arbitrary quotients= and as reduced quotients. Then you can prove that they are isomorphic and = that one of them gives you a field. Then you know that the other one is als= o a field. You may be interested in the actual definitions of the operation= s, but you dob't usually care about the actual proof of the properties.= So, you construct the addition and the multiplication explicitly, but you = get proofs that they determine a field "for free" from the other = definition. If the proofs for one of the definitions is easier than for the= other one, this might be a significant simplification.

Regards,
Valery Isaev


=D0=B2=D1=81, 3 =D0=BD=D0=BE=D1=8F=D0= =B1. 2019 =D0=B3. =D0=B2 22:13, Michael Shulman <shu...@sandiego.edu>:=
But does unival= ence a la Book HoTT *actually* make it easier to reason
about such things?=C2=A0 It allows us to write "=3D" rather than = "\cong", but
to construct such an equality we have to construct an isomorphism
first, and to *use* such an equality we have to transport along it,
and then we get lots of univalence-redexes that we have to manually
reduce away.=C2=A0 My experience formalizing math in HoTT/Coq is that it= 9;s
much easier if you *avoid* turning equivalences into equalities except
when absolutely necessary.=C2=A0 (I don't have any experience formalizi= ng
math in a cubical proof assistant, but in that case at least you
wouldn't have to manually reduce the univalence-redexes -- although it<= br> seems to me you'd still have to construct the isomorphism before you can apply univalence to make it an equality.)

On Sun, Nov 3, 2019 at 3:57 AM David Roberts <drober...@gmail.com> wro= te:
>
> Forget even higher category theory. Kevin Buzzard now goes around tell= ing the story of how even formally proving (using Lean) things in rather el= ementary commutative algebra from EGA that are stated as equalities was not= obvious: the equality is really an isomorphism arising from a universal pr= operty. Forget trying to do anything motivic, when algebra is full of such = equalities. This is not a problem with univalence, of course.
>
> David
>
> On Sun, 3 Nov 2019, 10:08 PM Bas Spitters <b.a.w...@gmail.com> wr= ote:
>>
>> There's also VV homotopy lambda calculus, which he later aband= oned for MLTT:
>> https:= //www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hl= ambda_short_current.pdf
>>
>> On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters <b.a.w...@gmail.com= > wrote:
>>>
>>> I believe it refers to his 2-theories:
>>> https://www.ias.edu/ideas/2014/voevodsky-origins
>>>
>>> On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt <= ze...= @fromzerotoinfinity.xyz> wrote:
>>>>
>>>> In [this](https://www.youtube.com/watch?v=3Dzw6NcwME7yI&t=3D1680) 2014 talk
>>>> at IAS, Voevodsky talks about the history of his project o= f "univalent
>>>> mathematics" and his motivation for starting it. Name= ly, he mentions
>>>> that he found existing proof assistants at that time (in 2= 000) to be
>>>> impractical for the kinds of mathematics he was interested= in.
>>>>
>>>> Unfortunately, he doesn't go into details of what math= ematics he was
>>>> exactly interested in (I'm guessing something to do wi= th homotopy
>>>> theory) or why exactly existing proof assistants weren'= ;t practical for
>>>> formalizing them. Judging by the things he mentions in his= talk, it
>>>> seems that (roughly) his rejection of those proof assistan= ts was based
>>>> on the view that predicate logic + ZFC is not expressive e= nough. In
>>>> other words, there is too much lossy encoding needed in or= der to
>>>> translate from the platonic world of mathematical ideas to= this formal
>>>> language.
>>>>
>>>> Comparing the situation to computer programming languages,= one might say
>>>> that predicate logic is like Assembly in that even though = everything can
>>>> be encoded in that language, it is not expressive enough t= o directly
>>>> talk about higher level concepts, diminishing its practica= l value for
>>>> reasoning about mathematics. In particular, those systems = are not
>>>> adequate for *interactive* development of *new* mathematic= s (as opposed
>>>> to formalization of existing theories).
>>>>
>>>> Perhaps I am just misinterpreting what Voevodsky said. In = this case, I
>>>> hope someone can correct me. However even if this wasn'= ;t *his* view, to
>>>> me it seems to be a view held implicitly in the HoTT commu= nity. In any
>>>> case, it's a view that one might reasonably hold.
>>>>
>>>> However I wonder how reasonable that view actually is, i.e= . whether e.g.
>>>> Mizar really is that much more impractical than HoTT-Coq o= r Agda, given
>>>> that people have been happily formalizing mathematics in i= t for 46 years
>>>> now. And, even though by browsing the contents of "Fo= rmalized
>>>> Mathematics" one can get the impression that the work= consists mostly of
>>>> formalizing early 20th century mathematics, neither the Un= iMath nor the
>>>> HoTT library for example contain a proof of Fubini's t= heorem.
>>>>
>>>> So, to put this into one concrete question, how (if at all= ) is HoTT-Coq
>>>> more practical than Mizar for the purpose of formalizing m= athematics,
>>>> outside the specific realm of synthetic homotopy theory? >>>>
>>>>
>>>> --
>>>>
>>>> Nicolas
>>>>
>>>>
>>>> --
>>>> You received this message because you are subscribed to th= e Google Groups "Homotopy Type Theory" group.
>>>> To unsubscribe from this group and stop receiving emails f= rom it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>>>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeT= heory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfin= ity.xyz.
>>
>> --
>> 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/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2= BaVT_aY59U_-9t17sBzeA%40mail.gmail.com.
>
> --
> You received this message because you are subscribed to the Google Gro= ups "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.goog= le.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS16Vy7sG= iEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.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://groups.google.com/d/msgid/HomotopyT= ypeTheory/CAOvivQz47kSm9WbKDmUsndrpAJMkNwiWmVABqOFrVqyTOvSAbw%40m= ail.gmail.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://groups.google.co= m/d/msgid/HomotopyTypeTheory/2ca6c47c-6196-4b45-b82c-db79b2b6568c%40googleg= roups.com.
------=_Part_963_1059132255.1572819805226-- ------=_Part_962_393102267.1572819805225--