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-yw1-xc38.google.com (mail-yw1-xc38.google.com [IPv6:2607:f8b0:4864:20::c38]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 20ded6f0 for ; Wed, 6 Nov 2019 00:06:12 +0000 (UTC) Received: by mail-yw1-xc38.google.com with SMTP id j3sf17762651ywg.5 for ; Tue, 05 Nov 2019 16:06:12 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1572998771; cv=pass; d=google.com; s=arc-20160816; b=xYwIGIGcA1qM+W5wHnNVO3CO3aC8ITFhYdwvMFH9cBNTahcRB1SdBzpdg1xhOX57a0 4qAPF7GBb0rKAftGiTsHweOP9CVRyKi8zSNTWFMdhC8PQ4nAX9VqAQHMHKD5csxyR6GR 0mZBPrhWySz/EIcNkF2w/EGZwRNyvizhz8kIQuu4Y18D+mcuqsUixVycyK0JGCCZVt+j 4sOb/wY1fOP6WlI6P95lFJyM3NGmiOVbTS48drRW57AoAt4HBDDaAIm8oPh4D9IpZ1EK 81zfdx9LiImkMzL/84aD6SBsVru+rCevvM8v4ffELUBy4hoTd8W6PtHaoFlvqzE88qgd S25g== 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=DLpncwMWRYNoDW7pjzsNns/M5R4cA9pdtmpViC7zcvA=; b=nto1uOk/XDHs7rEo3J9VMUlJ+Lxit7CEqoZ8VcKKA3+PtRzMGOJY+r9NMU4v9uuW0+ P0DKqXvulzT+o+08rLT3Cva9nY6PIX9l2WkFng/Pr2CTL84gTqbjdIg7Vxq7T5fvMfAN dJjpfoJhCc/rSnV46hrpz0Qjq8aeLy8L8IFJa30x7yFOMqOSdBxs4Cod8llhSjB3CQSS Y5bGOSOJjLmoikID7F+wEFgju3Vq7JuXo5VvzjWNDXGTxqD6fgWH+BdFatl/mzLsT26L 3KtxhYkIKGwp4Mbj0V0EJ7lAWPKLtn3zxP1uce4NuKtiCTsTAN+F7kKZD0Am2Xo9dv5f yZOQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@iro.umontreal.ca header.s=mail header.b="I/Qp9Baf"; 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=DLpncwMWRYNoDW7pjzsNns/M5R4cA9pdtmpViC7zcvA=; b=lHFzSqXx8snZ4jW+Bdb0qzzGfOGQ7nbzPCJ0v88Khx13d421M53XW3pVWj2llx4emD 13BcsrPYGFPZkteUCBd+L+5e6aolV9dF62P+EplkfNT10b9y5ko0RmiAw8Aix6/1P8xV AfCrej7b02ykjm0mQoJk93x6FiEb4294RxylfZlIl9LhmZE8I46sG9dru1O+5i3jcKPU 0UUkfohC2qXw6QmzyHmkITU3FNjv7z0JzkGdwyHtMB/lMJ0m65nAzkEfDsp05CQdJx+4 tYY5io9+JSSW3X7LLZ1zLIh96//TCopmrJOunzTxs5A3GNC1IymmDmZIK+w+imKBg4en x2SA== 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=DLpncwMWRYNoDW7pjzsNns/M5R4cA9pdtmpViC7zcvA=; b=oPAIPfSEOoUZax/rv/4HnI1Ie9aTyMNX4F0qziNXKwMHwntPIvw/dwOkZZm6Oh2jBC Qh/fqwsz1p7Qn+/VKPDSLVmz2ligr48uhhpIJp4ogCW2NJGtLDj5H1tWb/0aLLabBaC1 Fc3LSE2ULZgA06faCTlj1zHTeEbLarBlfzPvq3cGhqA/gutgOqyhGatY3pTZcYmWq3XK 9pnhLrK6IhGdC7qZuTcDawxyUQ6qowlE9PX1C/0QWhSDSiZ5zbyX/5e3QF3cug/BaKqE XglWEN1fj2/C3nKatTsp1zPNUGriQzq2L1m9IrHMgsjV2CctH3e0oqm4uJbfP/hv9Up2 SsGA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVsYoNTmKgretSHgHihT8tBdY33QE8cDdjcgJHjiEpoPyb7LPkR tlf50vMEy0fZX4f45V2ICL0= X-Google-Smtp-Source: APXvYqy3qWBxHC/TAuvWNEDrBLT5dGF7UmPpUvLQ1/5bnJXkESu5z/6clRdhW+ILEB0aSBBWJQPWxA== X-Received: by 2002:a25:c9c6:: with SMTP id z189mr17478750ybf.389.1572998771287; Tue, 05 Nov 2019 16:06:11 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:adcd:: with SMTP id d13ls104670ybe.10.gmail; Tue, 05 Nov 2019 16:06:10 -0800 (PST) X-Received: by 2002:a25:d604:: with SMTP id n4mr30416591ybg.466.1572998770800; Tue, 05 Nov 2019 16:06:10 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1572998770; cv=none; d=google.com; s=arc-20160816; b=u6sYF5apLXX3grGd/VCZlSbIBMVJ8AptEE0BbRU+wMRsVivGf5117NfY12MxFiApdk GXGEvaLiRJBvdrHDpCXPMdrf/Wn4+BSoSiL+wXCxMDVxnG0aiVqjcOu1PrO2EYJsrv9o zrGi5QkrYDvW9fnDCdrWomij0X9pZnNKQz3d28TFIcixvl2lk8OrYgiGezQjwsaBDICF 1ofZdpqiU2xVTOlo1eMlmWypKotF9tsEjIUg8W4Er5hb5SakxMvzTZN2ecFAnx1dTCCX DVLLuyHVbaOl4IYocjojcs7i+axp9NMaGezInfrv7bFQHSTo+FiK3ayz8KZ0ioxXfTsh JMPA== 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=DLpncwMWRYNoDW7pjzsNns/M5R4cA9pdtmpViC7zcvA=; b=Z1TJjxU+02C1jXlsf2pJp936i9QUqVCGabK5Nt62GbHi6d2Lkeivf85b8BTFr376NP N5A7Zn/PAMTyH0fSqcFcbLmINfCk/cx/TQbHqV+3EAI6kuAqPjg8idg5A2aefaoLk0on 9fiXVvjl6PZMH6N9dq0BaWD1vG25kVRNweXWIUc2rVicIna9IY60OiIJKulT6cWbn3An Y3iqKR5cFfMaJ1ibSTDXfyA+mJ3wan9abgnKflle6Exz6l9eLxi3Av9VIrOZcvVyB0Kz djlPZIxelpDY/iCP3Mb71sW+mvLZKf+Cc4qFSQVyfxteQgRQIUABZyGnhyRFF81vjYeM j2nQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@iro.umontreal.ca header.s=mail header.b="I/Qp9Baf"; 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 63si284099ybe.4.2019.11.05.16.06.10 for (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Tue, 05 Nov 2019 16:06:10 -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 pmg2.iro.umontreal.ca (localhost.localdomain [127.0.0.1]) by pmg2.iro.umontreal.ca (Proxmox) with ESMTP id B64D781249; Tue, 5 Nov 2019 19:06:08 -0500 (EST) Received: from mail01.iro.umontreal.ca (unknown [172.31.2.1]) by pmg2.iro.umontreal.ca (Proxmox) with ESMTP id 6771480D58; Tue, 5 Nov 2019 19:06:07 -0500 (EST) Received: from pastel (unknown [216.154.47.134]) by mail01.iro.umontreal.ca (Postfix) with ESMTPSA id 2EB2612098A; Tue, 5 Nov 2019 19:06:07 -0500 (EST) From: Stefan Monnier To: =?windows-1252?Q?Mart=EDn_H=F6tzel_Escard=F3?= Cc: Homotopy Type Theory Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Message-ID: References: Date: Tue, 05 Nov 2019 19:06:04 -0500 In-Reply-To: (=?windows-1252?Q?=22Mart=EDn=09H=F6tzel_Escard=F3=22's?= message of "Tue, 5 Nov 2019 15:14:07 -0800 (PST)") User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.0.50 (gnu/linux) MIME-Version: 1.0 Content-Type: text/x-markdown; 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="I/Qp9Baf"; 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: , > members of this list. The constructivity of univalence was an open problem > for a number of year, and I would say that, even if it is solved via the > cubical model, it is far from being fully understood. In my case, I still find it odd in a situation such as: data Foo : Set -> Set where bar : Foo UnaryNat since transport supposedly allows us to take a proof of equivalence between UnaryNat and BinaryNat and turn a `bar` into something of type `Foo BinaryNat` although I can't see any way to directly construct an object of this type. Stefan