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-yb1-xb3d.google.com (mail-yb1-xb3d.google.com [IPv6:2607:f8b0:4864:20::b3d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1072d13e for ; Sun, 3 Nov 2019 19:46:33 +0000 (UTC) Received: by mail-yb1-xb3d.google.com with SMTP id a200sf11151596ybg.3 for ; Sun, 03 Nov 2019 11:46:32 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1572810391; cv=pass; d=google.com; s=arc-20160816; b=H8iDSIaxYTR6x66RShRLcyTKutu+VXsTFNoW8yyXVPLlrz01N40k5kmIZLpFwwsrs5 OIfaFKB8cL8DcVwylAdtwYOffOkXCIJypjPvFgLeeiEFADRLnwOaIMhrCkUQyUJurq4s RZHQ1fxF0scvNORjy1kD1wdO1eP/u68QuV2sSh107MyriTMBOOIi0jzXl6vGWgnnGUGb 4H020y1YkfQ1JR4nBuL76fMKwIEEpdoyp9DFzOVHFLJbwKwyqHcxtp/M2Bn9scZhrCTz vHOq0vOS3o/GTLjAFupZk1I2NeILtw979SgEsEHe0VwMzz7gTXyyCbL/YKQ0kBXG3h73 eNig== 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=Dn/DRB5k5SgV/xQTmNg+0ene1StvgGTdLGT1hL/UdcM=; b=y3DF0X9IHBWxQtpwtVvTW7GPIjr4dwk/Da50ZLv84z6jVKbmUJbBiFBzyzEW+Iu8Vm franebVc3+9xHHLQVMVOzsCmjB5M/Ills9wFSRuhGrj7baP1/etRkHPjjxKM1j+hRR+d mP4eB9/p7yKjXB3VWCi5lLI7ZicAin5akP7NSqO60w+y7Y22CN0bXTbl0k65Q5DuZozE ByOYNBXto8BAIbP9NOWJVIp646bTpiVEb9FJq8U5Bg7V0xSqwLkBAAG+49stAc5HO2pP W+7Z2w2p83OeM+nA5c0PJzfI9+32QSQ/vpGMsUhHgvrY8t4zG1A3+/Gft7dC6IZtEGFc UlYQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=nANZB9Lt; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::129 as permitted sender) smtp.mailfrom=valery.isaev@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=Dn/DRB5k5SgV/xQTmNg+0ene1StvgGTdLGT1hL/UdcM=; b=rRsIawDVPBEYMSkqxYtKMOvaF1uarRK+FxMQjXoCFTAhA2QNtIEPh5H9+s/cZJZHpC jvNkZk2ZGyk6DLm73yhhBhJe/coUf3rX/4zdJfD/Lg3i03RoNokyOBZ81rJDMLSUXzK+ D7evaP/jn9ZPDsgXHkHdhO8S5hmFa0+qRV+JKJHReejvoINu4CwaUIbn1YWhS4N5tl6R ZIetUgtDplBlIGGlGt2JU3xHTvbl32QV73IUd44917FmZjDy7vNCu6mdEAKmYJHE7LGY aNB1PCnqhJFScgTxRoaF9MSGIpZcjejZqiqyVLAXbU5eBWgpAQbBPkfcPpoTChwe0q/+ Nnog== 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=Dn/DRB5k5SgV/xQTmNg+0ene1StvgGTdLGT1hL/UdcM=; b=jvU0AkiLt5KXgGI028zFH1gF8rdAbcsAQyFJDgNMWT5+q7x4Wx2ioLgj/T5+MPTZ/A kgQFBEWQi45omG19Lj3FGRbcyGJCPW5IxmQacOSvjahZ1JpNtdcxaoULVFEqJoVzJwzY BWb7OAhIYkhtlIPm+6YND5URDEA5xR0pdOGpAiUfX+kKwd2MTKspvpde0u0PY/nFjSnU Uejqe7rZsAGy5MbOB2z3aTqC4IGvfjbjgTQAZDQY5bfQ2IpsvOAJLC3lWR2z112hNuhN i506Ow3ZMMN+pAr7t09GpV8ZlSP6JUvGEx92h9evD4eF/Cv3IKxx53jHCnaGprNTvN1t S1mw== 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=Dn/DRB5k5SgV/xQTmNg+0ene1StvgGTdLGT1hL/UdcM=; b=lLi8mJY5wYGufIIAr9GPGP1wXGKbXpNCEv5iWQQLVjO/e/5uNWyvFiKtYy19O+wUEP 62xXWsP100qZnSMY5gwMHf4ZQGOBvdo9Pl0nH1FIyW4bMQM8ydbqaoVfJARGUGrY1PdM og5Nd52eIcafkC7RvhS3U9QZYRqvyWeoJjSnWfHl3ubHS2ZKCN8Y3/6Rz0CqsnJ8F/Nq 9vNzhCpWq3AxPzKxjBSFSF5zBch5DBmVZIxWyQtL6sg0hDCdfk9TdjcCv/Gtbf+kbkjL bwRhnMCt0QOYk7qDK6vjde47iDZYHMOeYvS0/h/lK8YEDSfIi26bhovxcaifGxFaOt3t ERpA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVLDQBKogjk0RKhEK79ZOLV9EUrkkm6LFft5cM9NiYJBZ96unYR VGIrd1tkZmB4Trb/5DGMe9M= X-Google-Smtp-Source: APXvYqw9ZFHu0+GBpq83q/tHFbXCuqJK420XXDafpXwOGk9YFS4rd/hEAi9QiX6e005jD+5E/jNC+A== X-Received: by 2002:a81:7505:: with SMTP id q5mr7691425ywc.372.1572810391516; Sun, 03 Nov 2019 11:46:31 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:6b08:: with SMTP id g8ls2000387ybc.15.gmail; Sun, 03 Nov 2019 11:46:31 -0800 (PST) X-Received: by 2002:a25:2484:: with SMTP id k126mr21031905ybk.172.1572810390904; Sun, 03 Nov 2019 11:46:30 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1572810390; cv=none; d=google.com; s=arc-20160816; b=0QjbMY2LzYPRFTjraKmGOvoocLRd4kHCPOmqZ3ht7lm+AZV/e9WD8y0y+gNbc8VYnP 7S5yMPzODWCkZ4rSVIV+4q1mdj8KBJQFQtfmKUsP5r8MRZ1dmCWZGklGN13bu72CJS2+ g3dntgs+0kw1Ma+/QlvxldytUwCQP+AH+y8vK/jYchMTMiYRNEnmp6vXNha+StHD33gz 7gebkt9NqtudkpFEOnkTXoq2lkSjd8XPrpK10+h62ulG0eB9q87tT/6Vs+Ps7z1ynpQH U1NzecTuY8djQB7OaM1ixi59SzXlwIUmBrSGlX+opZFiaDRLPmwbtUV4BtMpa5BOGDJj 7pMQ== 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=Ucub96VDhUSW9DglnZZMRG1lY2NuOCJKaztjJIpGCic=; b=03RCYH36o7EjJwg2Uxdaquhia8xzSAvNUb7kuWXvJefotUOIKnCX/PuxVfjZs3yQ9d yd6I5oqikm0hcPD7geUCkwXcdExYD0lzpOI5E8iaFDPI2SeZcyQKvdzNjVuLe2oNiEfZ /f0XO7F08DaIH8CVI3oWXwn747u1OI0UVsDEh9JBqPEkcLKqkotjgziJjnH8Ntkcdjoc HQueP8ycUgeqNnHBrb5h1Vl7lYfG44Tt6EDUnHrQ4g/7O/JcHO1w07DkQ7xgAhdFuW7j F9HJyEkn8IgSfuWUnWJNcmVPNuw2RQsne+8WTy/qrMRiju67RNk85oQu3lsBx9TjbvPM 7NNQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=nANZB9Lt; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::129 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-il1-x129.google.com (mail-il1-x129.google.com. [2607:f8b0:4864:20::129]) by gmr-mx.google.com with ESMTPS id v135si838467ywa.0.2019.11.03.11.46.30 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 03 Nov 2019 11:46:30 -0800 (PST) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::129 as permitted sender) client-ip=2607:f8b0:4864:20::129; Received: by mail-il1-x129.google.com with SMTP id j2so10823784ilc.10 for ; Sun, 03 Nov 2019 11:46:30 -0800 (PST) X-Received: by 2002:a92:350f:: with SMTP id c15mr24205306ila.144.1572810390218; Sun, 03 Nov 2019 11:46:30 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Valery Isaev Date: Sun, 3 Nov 2019 22:45:53 +0300 Message-ID: Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? To: Michael Shulman Cc: David Roberts , Bas Spitters , homotopytypetheory , Nicolas Alexander Schmidt Content-Type: multipart/alternative; boundary="0000000000009bae220596767443" X-Original-Sender: valery.isaev@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=nANZB9Lt; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::129 as permitted sender) smtp.mailfrom=valery.isaev@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: , --0000000000009bae220596767443 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable The isomorphism invariance might be useful when you don't care about the actual stuff you get after transporting. If you have two different definitions of the same set, you can transport its *properties* along the isomorphism (that you still need to construct). For example, we can define rational numbers in two different ways: 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 also a field. You may be interested in the actual definitions of the operations, 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, Michae= l 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 > telling the story of how even formally proving (using Lean) things in > rather elementary commutative algebra from EGA that are stated as > equalities was not obvious: the equality is really an isomorphism arising > from a universal property. 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 > wrote: > >> > >> There's also VV homotopy lambda calculus, which he later abandoned for > MLTT: > >> > https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlam= bda_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 < > zero@fromzerotoinfinity.xyz> wrote: > >>>> > >>>> In [this](https://www.youtube.com/watch?v=3Dzw6NcwME7yI&t=3D1680) 20= 14 > talk > >>>> at IAS, Voevodsky talks about the history of his project of "univale= nt > >>>> mathematics" and his motivation for starting it. Namely, he mentions > >>>> that he found existing proof assistants at that time (in 2000) to be > >>>> impractical for the kinds of mathematics he was interested in. > >>>> > >>>> Unfortunately, he doesn't go into details of what mathematics he was > >>>> exactly interested in (I'm guessing something to do with homotopy > >>>> theory) or why exactly existing proof assistants weren't practical f= or > >>>> formalizing them. Judging by the things he mentions in his talk, it > >>>> seems that (roughly) his rejection of those proof assistants was bas= ed > >>>> 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 form= al > >>>> 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 to directly > >>>> talk about higher level concepts, diminishing its practical value fo= r > >>>> reasoning about mathematics. In particular, those systems are not > >>>> adequate for *interactive* development of *new* mathematics (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 community. In a= ny > >>>> 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 or Agda, > given > >>>> that people have been happily formalizing mathematics in it for 46 > years > >>>> now. And, even though by browsing the contents of "Formalized > >>>> Mathematics" one can get the impression that the work consists mostl= y > of > >>>> formalizing early 20th century mathematics, neither the UniMath nor > 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 > HoTT-Coq > >>>> more practical than Mizar for the purpose of formalizing mathematics= , > >>>> outside the specific realm of synthetic homotopy theory? > >>>> > >>>> > >>>> -- > >>>> > >>>> Nicolas > >>>> > >>>> > >>>> -- > >>>> 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/e491d38b-b50a-6172-d= ca9-40d45fe1b6d2%40fromzerotoinfinity.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%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com > . > > > > -- > > 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/CAFL%2BZM_%3D%3DiLS1= 6Vy7sGiEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.com > . > > -- > 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/CAOvivQz47kSm9WbKDmU= sndrpAJMkNwiWmVABqOFrVqyTOvSAbw%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/CAA520ftr3b4cGi4vXdmJL-GbAVksV9ggrTAmqZ4E75P-ch1hVQ%40ma= il.gmail.com. --0000000000009bae220596767443 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
The isomorphism invariance might be useful when you d= on't care about the actual stuff you get after transporting. If you hav= e two different definitions of the same set, you can transport its prope= rties=C2=A0along the isomorphism (that you still need to construct). Fo= r example, we can define rational numbers in two different=C2=A0ways: as ar= bitrary quotients and as reduced quotients. Then you can prove that they ar= e isomorphic and that one of them gives you a field. Then you know that the= other one is also a field. You may be interested in the actual definitions= of the operations, but you dob't usually care about the actual proof o= f the properties. So, you construct the addition and the multiplication exp= licitly, but you get proofs that they determine a field "for free"= ; from the other definition. If the proofs for one of the definitions is ea= sier 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 <= ;shulman@sandiego.edu>:
<= /div>
But does univalence = 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 <droberts.65537@gmail.com> wrote:=
>
> 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.spitters@gmail.com> wrot= e:
>>
>> There's also VV homotopy lambda calculus, which he later aband= oned for MLTT:
>> 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 <b.a.w.spitters@gmail.com&g= t; wrote:
>>>
>>> I believe it refers to his 2-theories:
>>> https://www.ias.edu/ideas/2014/voevodsk= y-origins
>>>
>>> On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt <= zero@fromz= erotoinfinity.xyz> wrote:
>>>>
>>>> In [this](https://www.you= tube.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@googleg= roups.com.
>>>> To view this discussion on the web visit htt= ps://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-4= 0d45fe1b6d2%40fromzerotoinfinity.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.co= m.
>> To view this discussion on the web visit = https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2= BpNK90XtFk%2BaVT_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.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS16V= y7sGiEqNkCxOMYL4j%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://group= s.google.com/d/msgid/HomotopyTypeTheory/CAOvivQz47kSm9WbKDmUsndrpAJMkNwiWmV= ABqOFrVqyTOvSAbw%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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAA520ftr3b4cGi4vXdmJL-GbAVksV9gg= rTAmqZ4E75P-ch1hVQ%40mail.gmail.com.
--0000000000009bae220596767443--