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-pg1-x53a.google.com (mail-pg1-x53a.google.com [IPv6:2607:f8b0:4864:20::53a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4955288e for ; Sun, 3 Nov 2019 19:13:24 +0000 (UTC) Received: by mail-pg1-x53a.google.com with SMTP id b71sf11318756pga.0 for ; Sun, 03 Nov 2019 11:13:23 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1572808402; cv=pass; d=google.com; s=arc-20160816; b=lSpTrMXJD3wO6u+doSLtn5kt+IZXrUzEzzFtcTm8nigmSvUfD0rxE3JPW/xryr6ItK ZcojhFeKK9JSFXMaHjeWur0yOdcQnZZTto4mQZI41RyngtN2ntLT8vdFrbxxAUu+0v/K P69Sz2Q4LXpw/9SAjj8ZDT8jWd2+sEQ2ShJ6wI4zvGuQru57wGL0aSnkkfqau44r9Ssq ANXZikd4UGgEi7Ts+GM3gAxa8wFuqs/DwCofB746fbCxouH5BQH5LV4cKjFUhGNKESYX edawgR7yHXXLtboabykoauYqyVwGeCjvmJknepBUGQ24bvAgiAZgq0h7jE/M07u0TcE8 6DRg== 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=1o7BYRBMQoyLKpeWKs5yjbB9pfn2jSgMFhuFgbYDEBk=; b=qfeZ2eQxTGETT7bavuVR++Am4Urq7/S0uHEg27F2A1H2Cpb4ZwxlbpJ7kecNmE/W8F No7U7oXPppEkONVdVhYwUKupiuKN+KhF4UNSFU/+j9WmL1XjkhRlT58ndE6k1bpvDM4U DNAiEsKIeDuxTXm4eIOxcNr8o3FeJuWf6OiMaBI9vjg50tK0ZX4X87GM2Ax3Fy3ejc03 JUuRlcGhkF+LWmhj/vFTktxxyxSdxOpx9lgaK237OV+/L1xWAz9rvfySYhV4F1Cwowhn 3hvC0GswTyhTUkqslfOt3//owYNbSgvUkUU94SrjimPziWFZMCZQcGn/4A6+kyjoYnPX Mclg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=vakzO4yO; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c32 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=1o7BYRBMQoyLKpeWKs5yjbB9pfn2jSgMFhuFgbYDEBk=; b=Yk9yuqjYhR+hvK/QlM2FVI9fYgH3117JGojcMLx8ns0DN2GGSZ+K3EMr0mJdDuagtH xaf1QjXrTohNd8g98MI5rojXSRd+rVi2tjUF9TSwD/fRkNscT9mM+DLjCij/BfXLji65 RzvOzNydrpK/UcpTjvfxuAHvaV3DHawEDPPVw03rOJ3eY5N04fkkv2h7Uq7RqulX0k17 wi9/6EDkiN3yXeW22cgjDiZrP/3KZWWSFbC0JxYky83rFPCoPW2C/h9HJp9444Ptvsc8 5cO/ZRZOSFsGy1cwpOW/QGm6XamC2leR51UV2H8zL1gelvNkRX5q0WQ9LvsNd9OQI0go 0S4Q== 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=1o7BYRBMQoyLKpeWKs5yjbB9pfn2jSgMFhuFgbYDEBk=; b=sPUSnWAUJUvfJNmsZlyvwhWDCCWviu2QFDdw7ljxJoxMlSvQed33aZcTTTFDI7Wfdz cVNX1zddLn8asrQDzYkXDwEwoXI81/ZGDVAIipYNRUAdizY9oG9v7Egj5qJAzdBQ71/K 5DkoCXaracNKA0bgJrPIXUXssTBlHT9NCMLrNTN78bqaEqDr4zPIEwgm15KBLpJkEDn8 UyyBEShe8D0B0g6hjP06BpgXyyHjvj3HPf678yWWSdaf2v632GadU2RzWpKbAxtPyFl6 49qhQHk0XSe0RhNsvglR4HwKWQdYrwK4kfunbQqkGMx08wwOd/2ezVT6OFRjggFJATQi SReA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUgLLfHdCyUFaYlnpcPGg5ecElL325qW9jngS7QuuPmLyzVobcr 54AFOmXYoW0IMIjK2PSMiso= X-Google-Smtp-Source: APXvYqyErSaJWdzI7LW4qwQ4pjih498wyIWOow9MtrhRdXrMqMcn0sipBtzz9Y4EKHxw/G/4h51VUA== X-Received: by 2002:aa7:9a96:: with SMTP id w22mr1944413pfi.162.1572808402373; Sun, 03 Nov 2019 11:13:22 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:8a95:: with SMTP id p21ls1255574plo.8.gmail; Sun, 03 Nov 2019 11:13:21 -0800 (PST) X-Received: by 2002:a17:90a:2470:: with SMTP id h103mr31329378pje.12.1572808401850; Sun, 03 Nov 2019 11:13:21 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1572808401; cv=none; d=google.com; s=arc-20160816; b=XUBsLsE/YTjOTBJD+tE5xrxBRApE2OEiwDS8IgB4fEVsKIc3vEEsRsLJxQ1mibMxmy XM0nV/ONm7dE4v1E2xYjE/6oWMkSkxlz0wR/tiRbQsgN117uSCRflmvTCVWd+KV9KNsX ViBQIXLcUNedWFev479YyVdFAPvLQ29AgRpm8zePzUKXBAFqS0wsTkkVDvxy0TA6HpCm 9hT9g3BCgdeKcHbiUii3V7hOnMgW6NuTOParo5n0PPM/TIqt0KcG6q4+cVADtqzBfnkx 5784TKqd2hwv6sSxOWnOcXc6MRg3WnXubLQ3M+iyvcv1lKd4Nnq+EL1tcxIA5L4LkfR9 L5Aw== 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=WG3SEEOTFIlm6ldzLYz+pZlkRfr29QlCJrAP7esOTA0=; b=zdKQOl4oUxbq8Q6bA+STd7E3u6Gdgw7uVQPfQm86qvRFhc9zP7gbBNpMCdSuwensIJ vkp1lFZudT4OoZFmGAEYMQQfGq6mntzeoHeCD9DhKkUVo66jSPce3exXJeWoYIkPcfNv lDaNltKsfOkcAtALwcJZjR8eexh+hLZE4qXa2BPHiVlAFDCsuttlIt0lTEv9vwH5S+Hc 26uSznmWGFr8IFhbqvXejXjAtMD5N3Vyo1rCVsa4SBBeexVmPq3LbarzE/t6PwYVRqUe j54EXe6ZfLrtEaHzlUu12c/EBoRwIvUBkONNDAiefRehbzppfpNSH4ZqsJSRSYeMU1A0 0FOg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=vakzO4yO; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c32 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc32.google.com (mail-yw1-xc32.google.com. [2607:f8b0:4864:20::c32]) by gmr-mx.google.com with ESMTPS id s144si470421pfc.5.2019.11.03.11.13.21 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 03 Nov 2019 11:13:21 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c32 as permitted sender) client-ip=2607:f8b0:4864:20::c32; Received: by mail-yw1-xc32.google.com with SMTP id i2so6093700ywg.13 for ; Sun, 03 Nov 2019 11:13:21 -0800 (PST) X-Received: by 2002:a81:2142:: with SMTP id h63mr17571134ywh.304.1572808400632; Sun, 03 Nov 2019 11:13:20 -0800 (PST) Received: from mail-yb1-f174.google.com (mail-yb1-f174.google.com. [209.85.219.174]) by smtp.gmail.com with ESMTPSA id n185sm4599298ywf.86.2019.11.03.11.13.19 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 03 Nov 2019 11:13:19 -0800 (PST) Received: by mail-yb1-f174.google.com with SMTP id i12so826213ybg.2 for ; Sun, 03 Nov 2019 11:13:19 -0800 (PST) X-Received: by 2002:a25:d146:: with SMTP id i67mr2976360ybg.269.1572808399501; Sun, 03 Nov 2019 11:13:19 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Sun, 3 Nov 2019 11:13:08 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? To: David Roberts Cc: Bas Spitters , homotopytypetheory , Nicolas Alexander Schmidt 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=vakzO4yO; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c32 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: , 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 wro= te: > > Forget even higher category theory. Kevin Buzzard now goes around telling= the story of how even formally proving (using Lean) things in rather eleme= ntary commutative algebra from EGA that are stated as equalities was not ob= vious: the equality is really an isomorphism arising from a universal prope= rty. Forget trying to do anything motivic, when algebra is full of such equ= alities. This is not a problem with univalence, of course. > > David > > On Sun, 3 Nov 2019, 10:08 PM Bas Spitters wrot= e: >> >> There's also VV homotopy lambda calculus, which he later abandoned for M= LTT: >> 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 wrote: >>>> >>>> In [this](https://www.youtube.com/watch?v=3Dzw6NcwME7yI&t=3D1680) 2014= talk >>>> at IAS, Voevodsky talks about the history of his project of "univalent >>>> 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 for >>>> formalizing them. Judging by the things he mentions in his talk, it >>>> seems that (roughly) his rejection of those proof assistants was 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 formal >>>> language. >>>> >>>> Comparing the situation to computer programming languages, one might s= ay >>>> that predicate logic is like Assembly in that even though everything c= an >>>> be encoded in that language, it is not expressive enough to directly >>>> talk about higher level concepts, diminishing its practical value for >>>> reasoning about mathematics. In particular, those systems are not >>>> adequate for *interactive* development of *new* mathematics (as oppose= d >>>> 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, t= o >>>> me it seems to be a view held implicitly in the HoTT community. 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 or Agda, give= n >>>> that people have been happily formalizing mathematics in it for 46 yea= rs >>>> now. And, even though by browsing the contents of "Formalized >>>> Mathematics" one can get the impression that the work consists mostly = of >>>> formalizing early 20th century mathematics, neither the UniMath nor th= e >>>> 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-Co= q >>>> 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 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/m= sgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoin= finity.xyz. >> >> -- >> 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/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBz= eA%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/msgi= d/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS16Vy7sGiEqNkCxOMYL4j%2BZFqKv5uJ-ivk= uemEg%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/CAOvivQz47kSm9WbKDmUsndrpAJMkNwiWmVABqOFrVqyTOvSAbw%40ma= il.gmail.com.