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-oi1-x23f.google.com (mail-oi1-x23f.google.com [IPv6:2607:f8b0:4864:20::23f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b91e7c50 for ; Wed, 27 Nov 2019 02:28:14 +0000 (UTC) Received: by mail-oi1-x23f.google.com with SMTP id c198sf10461942oig.2 for ; Tue, 26 Nov 2019 18:28:13 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1574821693; cv=pass; d=google.com; s=arc-20160816; b=qr4J8ZNheSZ5heWcru0TKN5VxT74PxHYAD0R59s2XN3SURnPf/42kqv8fBllXTJbp9 LuqcLergI7dEkQNGa5MWalCRkK8Oeg4sT2xWsv2RhiY5hK4l7Rvnq9zlLXIYVU5pIb9Q TLVNogwfLLCduVt+dckxVL2BaErN5Wr+0stlSTXlot6SmoN+DhGoQDEcFiq08eh7nRn7 NGxhJNmAute55TwFkUl7djPzG3vmByELTFPfPruFrn0vaDXbHgURM+sUltI0ez72yWyT ZVe7q/SnF++ZEwozy9Z9SdSvQjpXL1mJy+RsZQsfMZrmPPHoFuto4o7F7s6TNWmuxb76 z2uQ== 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:mime-version:user-agent:in-reply-to:date :references:message-id:subject:cc:to:from:sender:dkim-signature; bh=j/9HH7y3aG3JlfMH/V7LKvrvxmukDW8q+1qDZFd9lAE=; b=C7C6fDjEZ5Wy+v0EsLk4HqOpdfKHMoXblPvwuj1czFkW1MxsDARDCzNj5H6NCYobQa 9bylUfUtm//PHcag3ErPutxlI9aiAq4orxZ/GfZwcRTPRNEgTk/ZSk33GREY8tsiTuve SyKqs5JpK9r6aO8jvIlW1fTshldFsGI7L3m68e3mszK1GPrrkuZwJ0uWk9mmyMMiL7tf ZqFk/O7Sj1EqocHB2pN3+4ml1y7NGTLp3jYflr4i/tH1RCIsiHhMUDmhawnnJEr0c7qA Fclqup34ZhtL2gO9E7c9GS3+TWlkm4Mb9RRQUTpNoY/lK9ZDM2jnNmPL4SyRkpyD0lwB qRgA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@iro.umontreal.ca header.s=mail header.b="hY/PC89p"; spf=pass (google.com: domain of monnier@iro.umontreal.ca designates 132.204.25.50 as permitted sender) smtp.mailfrom=monnier@iro.umontreal.ca; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=iro.umontreal.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:message-id:references:date:in-reply-to :user-agent:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=j/9HH7y3aG3JlfMH/V7LKvrvxmukDW8q+1qDZFd9lAE=; b=VbQIZe84vkcI0lX+bveLJxcHoTU1KQBEk1OrJAJmqbhUjvAQ6pTM9vUet05Wtes7MW H3nvAyOj1lb+mliWtPmuxPc03yDLoB6pCYDMg6+/te1lfLSQB/r1xlYkt5sJc5NdSFwx Bqyxj8ebm/cPRBRVrfD+vtK1Gj1Cm6ElcrTAGI6db3l7I+1cymHwMdFv/gGDWz3aIzQF /8Tbc15ZX9jZYOkqCJApXUq+qIqP2bNCi/k0acjemPEgXwUXKtxWj/pxjmff8CRGiQ4m 53ImyZ8fZ2ng0JzJbgQLRbx0z+Zd474wK8H4tci0jSi6Iuv4onxZL2oO0ahDJBaHOxR6 zZUQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:cc:subject:message-id:references :date:in-reply-to:user-agent:mime-version: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=j/9HH7y3aG3JlfMH/V7LKvrvxmukDW8q+1qDZFd9lAE=; b=KqRqpy09O7pledKZpo4mGIB2RVb25fK9sVGACFIR0AZI5H2vAbfwxX5uY7njlsAWgE xcEJKy7EzNv9NP1RZlIo6nM45PU7+aDrsUs/qjILFQ0TqnhqTVk7lW3KKJfLpOUxSdPI 1fhMEvTAegkNBSIrn2+6aCWfuLkIYpc9U1wQ/msGaT+h91A22/68Xqct8L4S9igYJlok q0nlNksov4wTr7dq34x0G96l0lUgza9swd1MkPuDLzRRcEg6yyDHDwaFC60TmgZa6OVl VO7cTJBvVSY94h+lHZv80hLPbgT829hlY4V/VwmZH/D5DQu9rmmU3jrog14QXpJ+QH6G be/w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWmaJ2RRj+f/nIS78toSgTPyS9kmcHYu3sd/9dkaYPbkaRn3vV1 pH14WRZT/XWfW/isNO8qKXU= X-Google-Smtp-Source: APXvYqz7eU6//zaIdLzpPuIoI49/U3ki8yEKEB46acUaIPM4t9RDjhV3/wwgaq0Bl+I3wRUZ8/ioGg== X-Received: by 2002:aca:845:: with SMTP id 66mr1898695oii.137.1574821693104; Tue, 26 Nov 2019 18:28:13 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a54:4597:: with SMTP id z23ls3619641oib.15.gmail; Tue, 26 Nov 2019 18:28:12 -0800 (PST) X-Received: by 2002:aca:d0d:: with SMTP id 13mr2030089oin.44.1574821692625; Tue, 26 Nov 2019 18:28:12 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1574821692; cv=none; d=google.com; s=arc-20160816; b=S5q2SKcL6dgKwbSik3H8OJXf/OkMLyUCNfD8PjwBnviDKGGbmbI7aBl+HXbWbAoQBa C4wyAFEYHWPhsAdOu0hWYCqLalFgkUvNw7qVy9ykH7vxldNszR7cBZrQrQrBFaHgGbuk VlxaEqXL0IVXyNcHWuP8Aoej2dmi7FmurrsAbjyLB8FJg+ctfuMc9V4OLy4k6iRBZi6N y0ShOdaiosoQxhxaAbME+v4/D78cdcc2sp+NS+8maL2Wvv7mOCajNif46WiYOL9uTl4R e5LRO5aaBx8KqoZnD9kgrYbDo38yF4V6NC3O9mlUZg6srevnyvlCjIBmYSCZiML1HbCk DT0Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:user-agent:in-reply-to:date:references:message-id :subject:cc:to:from:dkim-signature; bh=cj1kvOcpiY7CISkoO+LsONAW83AQRBwFqpcdIFQwaQ8=; b=j9Aa5UGv5F7i/WjRVsuyxS+X65/9CemckohRJv0tprtAjwAnN/XG6L9qA+RUszqjmD 06MME5lvRHOSERRqZKa6KjQb6ZelmTHg7jZLGD8y+oZkcFAsVaW4BlBvpKWHXf3NM5QW Y+Odz2fce7GKzm+OLszfnvzutjWPRUVRkjjcX3vwpaBGhjvGRFbejZW648koCGnGxkJs diL+1qOlZNsxmU5mUDpVaTNVq1RvmTtk74IJXYiukKu5r6LcRD2gr7pb3GxZTAPxeWOr cspZBRrbEa7lhvXmh4tF7p6xNlIFbrsVYfVlpOJoWjEcRyGHvW/6SVbB0WelpGypGkUx N/Aw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@iro.umontreal.ca header.s=mail header.b="hY/PC89p"; spf=pass (google.com: domain of monnier@iro.umontreal.ca designates 132.204.25.50 as permitted sender) smtp.mailfrom=monnier@iro.umontreal.ca; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=iro.umontreal.ca Received: from mailscanner.iro.umontreal.ca (mailscanner.iro.umontreal.ca. [132.204.25.50]) by gmr-mx.google.com with ESMTPS id j26si478525otk.0.2019.11.26.18.28.12 for (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Tue, 26 Nov 2019 18:28:12 -0800 (PST) Received-SPF: pass (google.com: domain of monnier@iro.umontreal.ca designates 132.204.25.50 as permitted sender) client-ip=132.204.25.50; Received: from pmg3.iro.umontreal.ca (localhost [127.0.0.1]) by pmg3.iro.umontreal.ca (Proxmox) with ESMTP id E32C444A340; Tue, 26 Nov 2019 21:28:10 -0500 (EST) Received: from mail01.iro.umontreal.ca (unknown [172.31.2.1]) by pmg3.iro.umontreal.ca (Proxmox) with ESMTP id BD1C7449C17; Tue, 26 Nov 2019 21:28:09 -0500 (EST) Received: from pastel (unknown [45.72.167.118]) by mail01.iro.umontreal.ca (Postfix) with ESMTPSA id 732AB1210F3; Tue, 26 Nov 2019 21:28:09 -0500 (EST) From: Stefan Monnier To: =?windows-1252?Q?Joyal=2C_Andr=E9?= Cc: Michael Shulman , Kevin Buzzard , =?windows-1252?Q?Mart=EDn_H=F6tzel_Escard?= =?windows-1252?Q?=F3?= , Homotopy Type Theory Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Message-ID: References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> <13f496d9-1d01-4a2f-b5c1-826dd87aebf2@googlegroups.com> <8C57894C7413F04A98DDF5629FEC90B1652BA70E@Pli.gst.uqam.ca> Date: Tue, 26 Nov 2019 21:28:06 -0500 In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652BA70E@Pli.gst.uqam.ca> ("Joyal\, \=\?windows-1252\?Q\?Andr\=E9\=22's\?\= message of "Wed, 27 Nov 2019 00:16:08 +0000") User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.0.50 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" X-Original-Sender: monnier@iro.umontreal.ca X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@iro.umontreal.ca header.s=mail header.b="hY/PC89p"; spf=pass (google.com: domain of monnier@iro.umontreal.ca designates 132.204.25.50 as permitted sender) smtp.mailfrom=monnier@iro.umontreal.ca; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=iro.umontreal.ca 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: , > Maybe AI (deep learning) could be trained to recognise the correct > canonical isomorphism from the context (=the proof). Can't we define it more formally as the isomorphism with the smallest proof? Stefan -- 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/jwvmuciqcnn.fsf-monnier%2Bdiro%40gnu.org.