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.4 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,FROM_SUSPICIOUS_NTLD, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qk1-x73e.google.com (mail-qk1-x73e.google.com [IPv6:2607:f8b0:4864:20::73e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 85965341 for ; Sun, 27 Oct 2019 14:41:38 +0000 (UTC) Received: by mail-qk1-x73e.google.com with SMTP id g65sf7780514qkf.19 for ; Sun, 27 Oct 2019 07:41:38 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1572187297; cv=pass; d=google.com; s=arc-20160816; b=QhJBMx3ncY0VYYa8Y9YLKey1F8RXMOiqWu63IiEZVdFQZQJTZInKkP6qcI5VlBRwwo bb5DoVh10Q4SLXxHSK2f/jGInozxs7ba+UgAVDT7eme6Wf+3qkdENDlyv4a+FlX4X+1H 8wiWFxon7Se3xyqq7dJF1QOawzevDaYrPHVXIDQXxIOhwbVJhEmtVgbuadXFHEsAcUpJ PQr28rW/FQXFjHOaB5yaH7JM6hmzZlOonHX68X3UDGU5DNdKs9IIEp3F48hgoh2cmQwQ hU22dtB1NRYrU/KvLbXYdLF7wCpJtdrLs/nY/NOLKb+f4MkHtCeJgbims09rqldEGdah axjg== 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-language:mime-version:user-agent :date:message-id:subject:autocrypt:openpgp:from:to:sender :dkim-signature; bh=z4uit+bjJiys8fVFbK6z0Wdmcn+I/NOGKD5r+CEHLKI=; b=sZ9pEPnI70y2QP4E0gBZ9aeqfGTjdLDgPP4GMj41Vk3UkVm0oCWuNSKSkxBblJWd2Q rYiBAJB1hIuxyhnkG7BcDOrho9v7wEZCuKGA0lirsOErcMmvVA5PE7gTvKjyFSFfbDyF 1iWgBcUdDVI752BSezrE595H54fv7j09lzfFxDQE5pMGvvRN9lJGzhrCt//McOm3J7Ex u6icoSD9yVDWassGJzhGDjsVJgxsgpb3PqHLD/qqZLy5AygIochqkdTdt9Cz77OHnQBx 0AMiuLxlgWOGBKQ8ex6c8A2AVWBNs4sV/n69U2NTYhr5cAAtsMt4KTUXmvfxTq5Jx190 BXjA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=ABnonH4h; spf=neutral (google.com: 66.111.4.27 is neither permitted nor denied by best guess record for domain of zero@fromzerotoinfinity.xyz) smtp.mailfrom=zero@fromzerotoinfinity.xyz DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:to:from:openpgp:autocrypt:subject:message-id:date:user-agent :mime-version:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=z4uit+bjJiys8fVFbK6z0Wdmcn+I/NOGKD5r+CEHLKI=; b=bBPVHScZZqBd1aXRC/x3wYgp2zk37WVXrsiz9LJBvpiQ++lK/IqMErjKnx3BKbp2U+ XqyBVR0EtSg/iieUDZlk/eoXjyDmfIErbYMQIWtOGS9FZILrOvJ3oWET/UUbnT1waI8B m8b22aXFjXy0uvPSvtooQTXij3psjd5ElHuYIcp7mb/26NEIlGgwGBtvOg9gzTbpLdyw 1P2eAVNo/8GnC5UH9Ulg7+3Z5q6+Z+GTh+65PJH04gHky3onvy0RVgBV+3COMxvYIFV4 sZpv/am5qF/oB9r9lNY24+kcSe5aeBwRPneX8Ega2kOweK6HDNnrQ6yIZbtxHsHkdPG6 QOvg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:to:from:openpgp:autocrypt:subject :message-id:date:user-agent:mime-version:content-language :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=z4uit+bjJiys8fVFbK6z0Wdmcn+I/NOGKD5r+CEHLKI=; b=YlWhhBSxZWOcUi6qJ9EDAMetW37XOA2sQXaUi+/KphU9hDzBGCwvc3IPeOsiYpb5NT hYk/BNWtcGNEtTdpLItrDY81MC582CJouM9UdJ2sDQatixUCWS4/Dn1zuMW7vlrr9X8V RCfjuSvfCmWJbXU+2OD0AazeEe33c3vrs32BjLE1ltDHRPUFxEC/0g3RHAERQBFLpBYD 2N71zuepgej2d6LOQ8qkBsMPCw4otGcsVp/gIAeG4+kcJeILUFegOX0XgeLA69Ah2mGy Dfb6EQaQvMjMSz/z9CDVljlgV+WLHXd/gXXp2nzNbx7vvgwAavpHR8PNWut3CjX6odbV sv3g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUQHPtL+uLFRpvKXavmiwvNrShToRC7QYhGm9c/2gIq5r6iyvYY rjR+RsQLv8Eq1zPeqifMIKM= X-Google-Smtp-Source: APXvYqxYpIxfPL12SkPdCtzvh/g11JKaSlBSbnaMRjYlhxulUg7sLBuFVMS2th32/Ck+usON7IXiQg== X-Received: by 2002:a37:8146:: with SMTP id c67mr11754258qkd.380.1572187296859; Sun, 27 Oct 2019 07:41:36 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a37:ba47:: with SMTP id k68ls439619qkf.11.gmail; Sun, 27 Oct 2019 07:41:36 -0700 (PDT) X-Received: by 2002:a05:620a:1659:: with SMTP id c25mr11881333qko.297.1572187296442; Sun, 27 Oct 2019 07:41:36 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1572187296; cv=none; d=google.com; s=arc-20160816; b=eEY3+IfI21h9Bz57hSLCEvzucHSmZCarULb4Ow7VmiP3dfQs7Hv77hSP9qnu9v9mLL CnyjHubhIJn0qaHDsCah1JJ2Hd26HB8/YZaRXAP1C8nw3a2S3vKMW33IrawQM7wDuMQ0 Zp67wKtzC9V0vAoJIcRVwjksngaVXyUn9p5TsDmvD5FB3U7LFbTCXH5Mb6C4Bsdds/BB 6OLCEMKuEOukT4IzaM8ZD9ZRlp9k1b3huHkqsyuhK6IoUlc6qoES0cAGG/LG5WJNAws6 zRU4BHnbYgFhbr0Joueoa/IfZC7JcV632sq/bfWIpdPs+YG4fIKwDKznDS4aqhR3ejUD 1UhQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:mime-version:user-agent :date:message-id:subject:autocrypt:openpgp:from:to:dkim-signature; bh=xGpO+ex7CZw1LcO/+owjwhPER2CvQ9zsmjyQYlU5hPQ=; b=jbtBJdZzf9NDkIO8rwNjcosg/WfoOXZvPZO57uQuoabWOLIEM+1J0Ae/hT8JjBxD3I b1vKfzxGXnTcIIIOpv2oDg4gvVXI6XOs4IcoOVRSXKKtIi0k/hsM3ANte7f5gZV1McDb 4vbdpOeivpNEp5FaYyhzUTcrf0O6GyVTxhh/PlWayaTX6a4461B3yWtgUuObIXMNvt98 NHNvOcFgein7klAlPiXxovQmD3O4xYonDMwx7zDkD8kpOFdKA9tYE2oS+nxZiZnPua9L J8+mY+jUienmEDQ1jz5OWul6sfWHnHxNH8IJ2slMADY03pYk03l0Bz4zXWapeAStmzVC Hykw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=ABnonH4h; spf=neutral (google.com: 66.111.4.27 is neither permitted nor denied by best guess record for domain of zero@fromzerotoinfinity.xyz) smtp.mailfrom=zero@fromzerotoinfinity.xyz Received: from out3-smtp.messagingengine.com (out3-smtp.messagingengine.com. [66.111.4.27]) by gmr-mx.google.com with ESMTPS id t53si390799qte.2.2019.10.27.07.41.36 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 27 Oct 2019 07:41:36 -0700 (PDT) Received-SPF: neutral (google.com: 66.111.4.27 is neither permitted nor denied by best guess record for domain of zero@fromzerotoinfinity.xyz) client-ip=66.111.4.27; Received: from compute3.internal (compute3.nyi.internal [10.202.2.43]) by mailout.nyi.internal (Postfix) with ESMTP id 095A221A97 for ; Sun, 27 Oct 2019 10:41:36 -0400 (EDT) Received: from mailfrontend2 ([10.202.2.163]) by compute3.internal (MEProxy); Sun, 27 Oct 2019 10:41:36 -0400 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedufedrleejgdejudcutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmdenfg hrlhcuvffnffculdefhedmnecujfgurhepvffhuffkffgfgggtgfesthhqredttdefjeen ucfhrhhomheppfhitgholhgrshcutehlvgigrghnuggvrhcuufgthhhmihguthcuoeiivg hrohesfhhrohhmiigvrhhothhoihhnfhhinhhithihrdighiiiqeenucffohhmrghinhep hihouhhtuhgsvgdrtghomhenucfkphepkeejrdduvdefrdduvdekrdduiedvnecurfgrrh grmhepmhgrihhlfhhrohhmpeiivghrohesfhhrohhmiigvrhhothhoihhnfhhinhhithih rdighiiinecuvehluhhsthgvrhfuihiivgeptd X-ME-Proxy: Received: from [192.168.178.42] (i577b80a2.versanet.de [87.123.128.162]) by mail.messagingengine.com (Postfix) with ESMTPA id 6BA3ED6005E for ; Sun, 27 Oct 2019 10:41:35 -0400 (EDT) To: Homotopy Type Theory From: Nicolas Alexander Schmidt Openpgp: preference=signencrypt Autocrypt: addr=zero@fromzerotoinfinity.xyz; keydata= mQINBFvJ4kYBEADc6gIExbYsg80gNMo07bgYK3UTmnPeKeW2FTmPwvvb42d7OYdgf9oi/gj3 C3uYE7Oe0XSKIM97KQwKfnbmlSlyb88PR8Hl69/x8sFDHHNj72M8NpW0GCqGdkH1yNVa70Iy LbdQYh5drz3UrKEm3dz0Zzjh46mPTVommdIMnINYw6q6zNHzyJyojh15slHn2BoyjsfI4zCN tLKC3AtkfdRdI89CHhVvoALz0AWuMYgA3cHHPY0mcr4+lKIZNcXDZ7pqfEzYY2LpktwBmFNR RQ1gpknEV5sGbH0kbuTyoJh7t+QBQvxzRHInMdSMlzHMOWqZUs03fyKSOCicsqQQZwLJaBGq OLgB12wwMsybFT4KvJNQ6SLVktxotRDCHPMqlvHQG1hBGgr0q7PmjimCgkjgDeOrnhN7pUsF a0UzZw8Zr38WK+4/7gcxyig3wzGOQOrMDzAzRU8mmVw1Gc8UTYJmQlKmDb+6/escPmtS7lnE uzpsuS97T1K/gK7d/3oeLg9S4BxYQ9Xu9jB+0CD1BTo6+Xk+ArFt9W9xMOeynU4l2SYkPUJA RaY3mFh10MipO5XI/1Pgymfz0+zUV+menY1Aarc+vGQlN6LwsEJ+p+pRsVtbK5IpeCaR25IE 5qn0FVjIPHQsOUGrEnjh+XR2pEaKkOvkLYAA6kCeLoVC0pUOiwARAQABtDdOaWNvbGFzIEFs ZXhhbmRlciBTY2htaWR0IDx6ZXJvQGZyb216ZXJvdG9pbmZpbml0eS54eXo+iQJpBBMBCgBT AhsBBQkJZgGABQsJCAcDBRUKCQgLBRYCAwEAAh4BAheAFiEE79VnB8rIfzJqh4KB0/gD0ijz 9ioFAlvJ+8EUGGh0dHBzOi8vcGdwLm1pdC5lZHUACgkQ0/gD0ijz9io17g/+LgdPIjqg6hNZ hmiMDu3o06p+rnf2t/E1RPO4KAZX3MiV3RzuJNUHy97TdkohXg7DwR3qM3X4wNv0Vf6nwoa0 /JGqWoHqeMkZ/GN5DhRjm9ChNJdWYOEZCD0Kz5MqeRcqGb1hTldluiVOYqISYe3o2OSBF65g 0+FHjce3eePXcyOK9JoZs/vG0vw9o9WWTGOU+3ilP3se82eTgRExGP/u0jDl1IQST8n5B28H grx95toFhhy7rjOhFlMCmVOHnzluLoAQZDa75aFC+DCwpUPyIdialbfXegV+Ou6qktGIsSH+ jxOjViFcmFzbTLlXlXvyKz8bA55xyHbjzvhQG1R9fDVHtcXxRucBv6jGDCX63wrD/iVlna+F +2hJuFUnFGjfCKHAak4/xWPt0Z6HI21zQlbj1lUcyeTbhAhNERaIObqtV5+K5zgEF42WDoD2 SNZkrgntXQzLBBElE2bPDEwGsiUDhQuA+E2MXKeoX9UYIJkIsfttP+gQG3A4dCswoTQooKIu RlpympYx1WqutRajRHVcqEI35lIaFBmw6WNL+IaXq+wnIFLwpRn2j8MLneh+cFt9QecbHYUE WQ7Ic1cBsXT2XCxvfVVeBWjS39DCu2rPO25QGlVtzBDSPr9PB9HU4UJ5hGQaWRJbM8SZPbfH aBWTlgfZrVjcARAnpvETJhm5Ag0EXas88QEQAKHwMUPVSVcRZZckOn5bT+vly6XSCnAvVmz+ /UonRT8zIU+f6Kiz7YXTFVSAJX8zaycoQQYeaiV7bgtynMLyW8gpVi8+PXgtkVld5gN6+HjJ krSZA/5cUVCZggXPFKHoEwy5imvVwQ+R4SebHgMkFLwn27lgoiTzjG/OBr6jATYMJI1FYGa+ wgFV5LWmDbY+ZmdSqLx3uUVgf0+cyqbPNHbTprFCYQ+R4ou9kG1QKmDiK1jrjVxMPH0cRU0M ++FNsSjZPBvYnjyogJOdMEtAIZ8LooHBq+JPXnYcfoAlaO+FcmaHltI6QX4hJ91elJmziLM/ yWa1c0WoFM/7L67R3QgU2bGvMEknT755XyuuEBCjYALv15lAi5783VzNXtvANM8DqRn+42Xr 5Avjm1QAq81cSS5Or/80Lrbg34qIKOtTnaK6BQzRjhgS78+sR8SldgG0KzH9UH+rEEVDajr4 wc/8x3BxZ8OCtDs+dKfewJE19erOqq0zNU+06WoHKFjzDZYeHBpg7gx8M75Y3C5zOi+8Gehj zYGQtBaqmHu9hP/MH+w3Zi8Xx1F6nR6yYymSWk2leq2yAvjnA9wyN2GsZ+lRB4CmXAY/ZJ7W KbtQk34BwpatNDkciVEsBqjBcmnvlAhigIHARcoGJgMIoetHJdd9ma5xLklMqiwRMendExsh ABEBAAGJAjwEGAEKACYWIQTv1WcHysh/MmqHgoHT+APSKPP2KgUCXas88QIbDAUJAeEzgAAK CRDT+APSKPP2KlDsEADMNF6vOm+TsyO1vZIESpUdkVR1GPU4GC2ajMx8fNFdNfbpLojMc6En gxcTElbaBwoG4s42rJc4PzNZKrjyCQjpEyq8Stb6uYObZgOiTYLkk95vcvQRW3TYFvjmfrPM PmiffNqnEZcGQjFKA8uuwXFrKS6jbA8v6JF31e6R42RLf0dG2ldfG6q1f4AMZAeEScsWzawK +s3MiDybQalEdiWb02SS+4GV3CPlMPLiLqQT0axrffJpoCDljf45DgvtSY4blnaDNBgk2GOq ZTZ/i4yoWyleJLKE3uIOlS+z2ZK98p39S+PafM3ImY6EOKl8YlzXKKVWPWEswI0fQ+9BpWL4 Wc1MhpOG4PxNz2Xlt1dDXmK+9g8dWbRbqSlM7v5mu/GlATk3qDOVVwIo4yNptx6UlqHXa1V1 ivH1z5pK+Ud+PGz2sL6GjZ2GQjl4AoOBnViIx0oyvkXMaGO7INqoZniIsDeLrpLKBUvSH9ty 2jL4t8en2PNXHLXYl/sgKyY+WDl9qJR1IdG9kmY1+6idgweIWdtRB7A7K4Sg7vC8YZmt5var 1IRKkUKQFsGfc1b30fcuo8gs578FRjY2/FGyuEdC0odufvx0QLGTiOfQJV9ObmO+PFhEOEto 3a6E/Q+6YXYEzf8zMfVFD9xdDwdokc2RAMjstb9UoKKTG9UtopYCoLkCDQRdqz0WARAAno+Q fnTZvKaN7jFf6iLThezZLMUFj/aAIB2spxgswuzTBVfsPoiyFctjTyveq0aU4SAJ2wJkTHLC SvrhdZPoSA855QZLSm35wUF2sRnIs1CTjirrR4nyJEY+RA398PLB50ms5tS3ihkb5IYqC+7t phXYZy/se1GNTnTEnwleR+fA+TnfxlTlHOInej4ZPtmbCMGSu9/pnRLq/RBn55yGUJfb5dn/ uCKgcFYALYP1jeIqQ4ZCQA3j76GCo3jWbiX61O+QI2G/g38QrPwD511/e9jRFOW+dM/dgd2Y OqM2W/ACMLwV32RgjFN8zeHYTrc3JB5tLuEMBb9VG1s7nrkvKQL1VqMJDj6hG3HzWukvdQP/ JH8GgblQsFSfKxwRMjttCs/5xK3n2Evs49XHZ5tPHIalmYPiquGMXCHmF4Mjvi6PucE+TUXf 315ndfx2jj26yp5lhgh6XAlHzp97HxxVL7VLhiNQXHX47yQG/xYmwzbtj0q3nNV4/AYcG1FA qR9AAf0jdj9ASR/qJHpLlKqkfAeAx/CABFobk3b//s/uCjh5i+dBFzKQwFFFozaZT8VLPz5G 6s1y4fKNC3XG1JY1eS1GHQmaauWNLfSq4wTQuzhX1eKd3NoHwELB7ika7QCsMIIANXSzC8Lt A9zlr6+qITDEWpWDzvXJdqFGNF+mPnsAEQEAAYkEcgQYAQoAJhYhBO/VZwfKyH8yaoeCgdP4 A9Io8/YqBQJdqz0WAhsCBQkB4TOAAkAJENP4A9Io8/YqwXQgBBkBCgAdFiEEB2zkL9pJ42fx q5JuoOuNvUZtM1UFAl2rPRYACgkQoOuNvUZtM1W3RBAAnh/9/uz2Bs9Ny7yv7yha9/G5Ynfu BOc6+4ueW1eq8nD8VaZrNAg6g61ynizdExCrGaWmXdrJbt4EwP2HMEFM0ee6M02yZ7sv1jmo jv82pqs335MEG5mtnJfP4QaaoQsiCZwv9yXk3yY9mT73W4ObgM4pRWQ0xLGee8fgMCLBQsxi M4OcrwQy6C7zbbIjbsVH/ZIYmxsy5saLmfmh2MoQt1QwFJLwYfHJBWsr3NH3Z+YoZG+rhccw ZODVY3Dcbypy70P2WfVjTi+6u9n+uidkcaHaefSNUJVDLRMLZjRMYsHIx2hxt4TKowXYTwlO TYTliIIG6Zs2V3iYNKGBFpPKJUCyAVbfCc0UV1S3c/OSJQqbOiru+VwUsI77XqQCdx7q58DN cwUoOZC6HrRmE63I2w9yi9NphoFC5djrcjvu8kZfe5NPVMIkKZRKC9pVrazkgbEbp/jcDAgh zTBxQoMm7KizyB4x9kBe239JvMoUzgXa/P2jbnH74hSTrJAytKqEOLt6lDq5+ueKDRj7E8ri js4+Wb3WYk4oPXusnZt2hB7aX7RgJXDkmSmPXIUtG2FxgS0aoyfHhC7H154RdabgsUiKsyCT kqKGGz/VvC76OJl24OcdkZfTjrZjhVadkmMrwfrC31P9nF3JDj5TPzCLgWmtfxKDZCSpvTD3 LQmMapUesQ/+KCHt9Y196oqxunuXXGKFaHZ1FGMRz0mc9ftIDWT1Gymtmq+AnkXDY2zYQWlj j9p2p8vySzA+jBajWODrU72xhHoLSVLOn35K9xrhrn0yDR+u49BZo3y04CNJQW+RZheSOjQI U9O970rYhwIlx3yZlhJEzDzHA6xtDmIKQKCL/3yn/8VbM+j+/wi8XsOEUMTSWrjvsvTjO+M4 ZVW5i/2CNxQxRBlkWgUyacosZh6PQlNVrxn7egfIZVDSLgTFZ+bUvlyZFi1C0bu/Fdb4YYaN UKCHRpvxdKFOdTfXCQRin+rsvRGmXnizO673uc2i7doJseCwpkQqaSLrzQLID7W0p4BQ7F8K z8oeD1pjeo6guLLiVlSa8jboi9+3p+VgiTU4jsuXZBUwDk/5h3GvX1KAjFVNDymPFLfv0TIr iL0UATZl+09R9P1/Kv0Ul9XzOv0CvMOCZLeT6NY9KeqMZsWhdLuFZHnmXHKONqa5h+OxpYmT ucCRdHoe/BjLxjE3xDZkI1mKf4opAh0a8xDXBU+3Z4l1bOLIPs3c2PZtBK7DvvRR2DdWARHp frEkBDaM+01VowjVBpgHI3xrWt6cf45dfGLeHNmsTQMa20L2xVGQcg5REmidEAtaK1WTDhc6 rBjXfl19Irsz/n31mfUlBZtWag6QD9N/Jlbv1P6YnkeQ3mE= Subject: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Message-ID: Date: Sun, 27 Oct 2019 15:41:34 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.9.0 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Language: en-US X-Original-Sender: zero@fromzerotoinfinity.xyz X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=ABnonH4h; spf=neutral (google.com: 66.111.4.27 is neither permitted nor denied by best guess record for domain of zero@fromzerotoinfinity.xyz) smtp.mailfrom=zero@fromzerotoinfinity.xyz 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: , In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 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 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 for 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 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, 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 mostly 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-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz.