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.6 required=5.0 tests=BULK_RE_SUSP_NTLD, 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=no autolearn_force=no version=3.4.2 Received: from mail-wr1-x438.google.com (mail-wr1-x438.google.com [IPv6:2a00:1450:4864:20::438]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8a27f6c0 for ; Mon, 4 Nov 2019 23:21:02 +0000 (UTC) Received: by mail-wr1-x438.google.com with SMTP id m17sf11117118wrb.20 for ; Mon, 04 Nov 2019 15:21:02 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1572909662; cv=pass; d=google.com; s=arc-20160816; b=didqtPRFlJMJC2jlSVHdIWWBshH8g2BNOCqpM/qPotrRc3O7OUZpfxWs3OunygpnSq Gihw/7zh333g5zJxgGWLVCVr4VOm7ZY7VUApywgz1TSJc2fPiaCOWSlho7TSGRQYSQ3M PxPI1m6l6rOtZgrYBnimx8rKEIK2Iz4IYvIwQFOzZAbLODerfbj9/kg40diw5mBqS4mJ SByz2faIqbemNdYsrZO05vOQWA/0mriOzv2XQfD5+wbA0sSxPjAE3bHYwXHVLSN/o4Px 2AQ157ZHBluqKA717y3unyfmlDQJBc+hCuh0BSDlO/MvcNAXCuzMuLFL1L/7TSlkScFe PQ2w== 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:content-transfer-encoding :in-reply-to:mime-version:user-agent:date:message-id:subject :autocrypt:openpgp:from:references:to:sender:dkim-signature; bh=oZlZMK2Bowa7w+ZEV8M8jypOdeLkJ94BuQ5SbvqNgTU=; b=FuPoGyPIAQx+zGmTtPavMICTaGrLlbCXW/ibOTa1pGqfC5OwLLyGlmhaABeCZlhTCU Z20/HD+XrmzkWNFiknibGfCkSjLvaL/l/9JvyjX6CjhHGMGrmcSbORAXbbTNI53qLGM7 wJp9hNaZT8jSC6T/9+a3BAG6YroUq6iE5WduS3OxIrpfFnM8+OjnokP9u3dCsKlvKqtx v6CthwuNW3ZUUOv+KZxJ/DJ+sS9kZkBYUDslRr1ZFfco1GBgGZSibvxdHp2LhDYnn4Tz fHXir/9ico+UQIKHLoUjFyd5gPy9j6XKYCQHVNTYJYOwr3Z06QTtRWnvXRgKzwFkCSVG Q0dA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=ruhjDoMp; spf=neutral (google.com: 64.147.123.19 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:references:from:openpgp:autocrypt:subject:message-id:date :user-agent:mime-version:in-reply-to:content-transfer-encoding :content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=oZlZMK2Bowa7w+ZEV8M8jypOdeLkJ94BuQ5SbvqNgTU=; b=qhz80NGx3bTs6OnM4AX9tQat14JhCGbA2O0ID9Uk5ed9SNDVzDA1XXChoOiUNMmAeH bg0wBVixRq5+938BEUbFY+xDzGbFNohNVHC14rZU4Qm9fenNoNgAmboI71dxrMiysCBu tnaMk0T9YVeVGkd6VH+BtIKrgp8oIdv3xQe2KGlLLWOjzl4BM4X+i9ozCt+WiMY6rT5R /qsAhfG6WdWLQMbM7ileF9OKtGVziatEPn24GYQRgsac4MXfraPebdZpHGVO0SRHBuDW Cjo8i+BAZC1n9MFHHme6hK3iLoziiFhsGjQw5rHVN60jf/93QNOwPurTfZkv5pGU0rW5 lc4g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:to:references:from:openpgp:autocrypt :subject:message-id:date:user-agent:mime-version:in-reply-to :content-transfer-encoding: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=oZlZMK2Bowa7w+ZEV8M8jypOdeLkJ94BuQ5SbvqNgTU=; b=i9gqmDPUFtSG/2v7ktfcGvvUQycyo+WCrxslS17qe3y4VGT4s+XpaAwmGIBctQ/VMR VWm7Id+AQeU86mnI5/xdSeVfJ9C9+YToAeXsTl+H+3uWECFyaY1Z9opxgtrBVbVwnB+3 Cg9HF7Vzf8fE6Vxng5HpIlMRGocmSkxkvWfRuXMVjDz7rsL92ChrLah5MLhceZmQa7k0 j0WxDvCdY9ngXJ/lQiUB1UWJBCkOjefnCkZ/YbLxhKKFjgHXM/2kgZt4k+MMkqJqoEy1 SmrqzH0F3gscI0vy0dljpPeNTkvyGPMdaXZIxDb2eVrDkdoeX/szEkl2oskklCwy22DR g4dA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUnkaEGM3kjvNJzTPgDDPZY+WE+QAE/6pKV/YS6PF8rMwrFXS61 R3j8cLq7t8ICga5RuZPrlc8= X-Google-Smtp-Source: APXvYqx/Y5QyGeMEm4JBzogxrGQU70E7WTPdgEt80Cgou+otChUFZ14zgCtXeQ7unFPus2Jh0gC9QA== X-Received: by 2002:a5d:54cb:: with SMTP id x11mr25755822wrv.161.1572909662419; Mon, 04 Nov 2019 15:21:02 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:7704:: with SMTP id t4ls596511wmi.4.canary-gmail; Mon, 04 Nov 2019 15:21:01 -0800 (PST) X-Received: by 2002:a7b:cbd9:: with SMTP id n25mr1410345wmi.64.1572909661898; Mon, 04 Nov 2019 15:21:01 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1572909661; cv=none; d=google.com; s=arc-20160816; b=RwKOeJ+BtjFMm658ETyNfpX6UkYbQf9K6mJBOtYQ49S2WXtvyy84b/k3BAlSNkOREN oX9j+aWXslpp19ClxPMMGYrRy/A6tz97BazLlCBJmuKR/LXp24q1+M1NPq2NkwPWFw2q yXHIGJEf4vyTzDDhA6xZvPPZG8KPO9Ckee82d8Eshkm13IJrOvL4rHX7/sMYgEkaRUvu VHF2TY7OLrGxk7bIM5pol/QhhLeEtEVPSJ0c0rHY9Z90KDZzfP86Hr3X0m/xMCuT90Uj 0MJZDNNP58SXJcL6AM+nxXp9+mho0F0Fx1AYv1+PFUAq6imym110t9nGp4w48lYKKSjk ZusA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:subject:autocrypt:openpgp:from :references:to:dkim-signature; bh=WaLx44EoTkkbJZMr4C/ak1WT/egCGTo5p+URlC/s7ew=; b=Aqq9q9E7e0h/m3aVweq73hGwju1jMXzb8WsBkDKOBWkAlN7X7DrMh05rw6514bEdpI psByQUjWmKCSr7g/1xZfcy9riYXZP5+PFXg/GIgVWG26rBElT85yV8bJBZRnmRTe4RLh akLrwbGA+rnU+EI1ixwaURnRaGOq6cbMumcNLqifnatRr6blMr+kyErkA6yAXdgD330L egiJfM79HXK75ZWyWHeoUHZj75pEG7vSJ3LOPxzZpiPWdIIARqls8kTRPaq12GCOtPEh Qgy4yLNzlavoMtAxDc9vS67v9AoyxQjZgCuu3CKbr4afVGLRBoGWmpLVQMyNSLvkDzJR nZAQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=ruhjDoMp; spf=neutral (google.com: 64.147.123.19 is neither permitted nor denied by best guess record for domain of zero@fromzerotoinfinity.xyz) smtp.mailfrom=zero@fromzerotoinfinity.xyz Received: from wout3-smtp.messagingengine.com (wout3-smtp.messagingengine.com. [64.147.123.19]) by gmr-mx.google.com with ESMTPS id y188si786998wmc.0.2019.11.04.15.21.01 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 04 Nov 2019 15:21:01 -0800 (PST) Received-SPF: neutral (google.com: 64.147.123.19 is neither permitted nor denied by best guess record for domain of zero@fromzerotoinfinity.xyz) client-ip=64.147.123.19; Received: from compute3.internal (compute3.nyi.internal [10.202.2.43]) by mailout.west.internal (Postfix) with ESMTP id 1A0A22BC for ; Mon, 4 Nov 2019 18:21:00 -0500 (EST) Received: from mailfrontend1 ([10.202.2.162]) by compute3.internal (MEProxy); Mon, 04 Nov 2019 18:21:00 -0500 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedufedruddugedgtdekucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucgfrhhlucfvnfffucdljedtmdenucfjughrpefvfh fhuffkffgfgggjtgfgsehtqhertddtfeejnecuhfhrohhmpefpihgtohhlrghsucetlhgv gigrnhguvghrucfutghhmhhiughtuceoiigvrhhosehfrhhomhiivghrohhtohhinhhfih hnihhthidrgiihiieqnecukfhppeekjedruddvfedrhedruddtleenucfrrghrrghmpehm rghilhhfrhhomhepiigvrhhosehfrhhomhiivghrohhtohhinhhfihhnihhthidrgiihii enucevlhhushhtvghrufhiiigvpedt X-ME-Proxy: Received: from [192.168.178.42] (i577b056d.versanet.de [87.123.5.109]) by mail.messagingengine.com (Postfix) with ESMTPA id A903A8005B for ; Mon, 4 Nov 2019 18:20:58 -0500 (EST) To: HomotopyTypeTheory@googlegroups.com References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> 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: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Message-ID: Date: Tue, 5 Nov 2019 00:20:56 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.9.0 MIME-Version: 1.0 In-Reply-To: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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=ruhjDoMp; spf=neutral (google.com: 64.147.123.19 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: , Dear Bas, Michael, David, Valery, Mart=C3=ADn and Kevin, thank you all for your replies. When I posed my question, I didn't expect there to be so much room for debate. In particular, I am surprised that it seems not at all clear how much univalence actually helps the practicality of doing formal proofs (as opposed to any theoretical benefits). Kevin, I would like to second Michael's interest in seeing these 20 commutative diagrams. Moreover, I'd also be very interested in seeing your "spaghetti code" (quote from the slides of your Big Proof talk): it seems it should be informative to see where your initial approach went wrong, and how much these problems and their solution had anything to do at all with the formal system you were working in. Are your original files perhaps available somewhere? -- Nicolas --=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/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinit= y.xyz.