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-il1-x13c.google.com (mail-il1-x13c.google.com [IPv6:2607:f8b0:4864:20::13c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 736942d8 for ; Mon, 11 Nov 2019 18:26:20 +0000 (UTC) Received: by mail-il1-x13c.google.com with SMTP id l63sf8314076ili.17 for ; Mon, 11 Nov 2019 10:26:20 -0800 (PST) ARC-Seal: i=3; a=rsa-sha256; t=1573496779; cv=pass; d=google.com; s=arc-20160816; b=L5eBCnODf5qdfpGxKMVSvqMhsKHmrHYNH2WAXzPz1hEk2wFIP0Y4x6j/Xqw0kfQrXX VeVKpONaxXV+WUKR/gqVj03Zu5iXVPF4ENCIb7j3xKZQGdydJ8EgkRsiT22+xwtcVB6N HL/l+xy7AqHSIn2rsIMNC6nrM5zSH0w8Ez1L1bsp4b5mmXhfYBDE4KEDtw4vucKdz78b gXhgl9HSzpXaHclUpN1u1WvaKRraVgM0jYIpTsLL8Yxz+6ad4oH9FbZY5YzMHm5FQfhC avkHHBqLhoVcOCVzcA6lDuYyfSjT5m9JdEGTw04xrZ/N0w5qurw3uPng+50lu355nhDd WhhQ== ARC-Message-Signature: i=3; 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:content-id:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:sender:dkim-signature; bh=o8lcLFY5IltVkgc8cE2EpMR9hlHb/iUhd7f2rWLA6V4=; b=l2slBdYv8r1PaCSzAJ9oWqDkP7yBCSUCwSADPLAtJjo5H+i+ib+7nH6EAti5Qdscle DAQlRq5Rou0SG6ywVkFiSWZSSI866RW78nh+WgLKIYoJFlLfQnjnKGwKf07K3CUF8TJT e/BYSfSho4QQEVViI+Xzf/Vzjsdj0cxwNMF7PZ8wyn2sKy/LTJsr/oYHW/13aU5kqQMc YuKVz1Z4JTox0qe6+l7hw6tkO2hlsT8flpi6uHuKMSZV1MtjLSP7wWuudQFg+8MANAcf aeyJK7DwkdzYg6FUcWP4rdBTmvMXcsVxKkoT2fBydbQNzUm0nbh3QfmDWiUww495faxv qapg== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b=CEebtZPX; arc=pass (i=1 spf=pass spfdomain=wesleyan.edu dkim=pass dkdomain=wesleyan.edu dmarc=pass fromdomain=wesleyan.edu); spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.69.112 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:content-id :mime-version:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=o8lcLFY5IltVkgc8cE2EpMR9hlHb/iUhd7f2rWLA6V4=; b=AFC+IDbagghr/jcKkTRf4lWTv2+A2dmPtNRNIbGj10X0XjTmAM3ENNLlOVi6r5FoDw b+kQd9kUj1W/h18ZPlncYgq1tsxPwy3s6z3+PxzwxVxKiXb4NgYN60nN8pPPApn/pRCL KDUALhjhYRcRa9BxGB0YrKMVhZ6ELDQy2oLa5MCwkBZNdMLg2yzs511wJAmQW/nNLn4S /Oht4qXfPv2SWEr1HPMXMilz1cRRudElOVsKHdnErSdFzGHMUrefNdTaZWgvyrjVzK/Y 2U0HB4lt++O4A3ZqTJhwt0O2jegAjQoabM2BPWivbfsRHJxOfFtKiN/NddpqWeMhUqEi WCAA== 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:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:content-id: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=o8lcLFY5IltVkgc8cE2EpMR9hlHb/iUhd7f2rWLA6V4=; b=hZeyoHPuIc49rYqdQQA3WXTVnYSwCBne358w7Bu8VFie9glMbOlAB8AAMQ7V8GkmEe zEOsrM2DmYLHawZ0hZf1lKYSbHw37Qcj6OuBv7R94j4SduvrgZg3HnwXRDJFu5+z/Os/ 8svFrufck7qvkMRp5WhvzoyqIMXJglOZAca+YkaKifaWgH5gQJ0QuVakwVTWg0QhUn1x JUdYDrdMYrIbU3XdSVY8LaxiHuy+Rerl/PeJzkMOCzfEcETI/LWGAN/fIKi9Nrql3cdB dDs28CaEGEuQSDAoDp4t6RZiw6Vam57rvkxNSILe1EharCmQeSix8DEYpJXIuFjbRQPv YkZA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWSjUhXOpFdoUWSPP6XhqB6VCczN7MReowDb25CNBoskt4f1TsJ e+TS5IMVCBmVcW5VE4IXelk= X-Google-Smtp-Source: APXvYqyAJcyC4PjM0I2zHnnPzZrvK28GDmwSVnNzOiFHgI7n3MHGsmnUhLmP+sC+wkhAVq8DVUudDQ== X-Received: by 2002:a92:1711:: with SMTP id u17mr33434351ill.192.1573496779673; Mon, 11 Nov 2019 10:26:19 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a92:aacf:: with SMTP id p76ls1231585ill.1.gmail; Mon, 11 Nov 2019 10:26:19 -0800 (PST) X-Received: by 2002:a92:1696:: with SMTP id 22mr30678021ilw.243.1573496779241; Mon, 11 Nov 2019 10:26:19 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1573496779; cv=pass; d=google.com; s=arc-20160816; b=MWHHx3YCiKVLDG5RuxN10L57OUhyMyYOUofmP6gnojvcDK001hCOLniu4sbcvfJ5U2 xrM8KXNdJBU4PcyqlUJup/zmJSIBZv4xpju0bTbMhh60+tasnmJ1kgQnMzj7Itfpxk16 czlJjAjt2VdT5eMvRkV2gibS9qBC0MDzTNxo+luRTx+DsB1DCT9S6lCX6IrY5osg8xCS oF3soiyPSwYvBmnQET/eIPSo35M+N/tjBRkuNMK6b7QYPii1dc+t5iizMA8x7Aghw1LK NTWp2joioavf0yJlm8+Tr2n6cXQIlRi0t3PJVbEKLp7OlPij3vVtSwH3UM0bjrn3SlBz ixSA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:dkim-signature; bh=wXp+qEbA9azP6+APPbVVUVq/9WgH79MMCYtDuta+tlg=; b=xkxGQKggw5WU+AW/P9TU5UVSPsHcMkVaUnx2+9aJ39Caeb+bHJKX4EJtTvW3nswdIr rIrX8azqsnV1s/PkiSeIdVIwwOXyZbYG/cNiM9vv01hl5sAPqP2DunJsQrLW+II/nN+/ M8JCuhe3cvK3o+F8NCPFX/aRDt48okR7mThJJy1LtnqrYCsBpebU+fqTC108R4cpg7qJ sqxkDA+x95fQJ5qOHXColj64XIYLZpWPvEeaLTgIqDWfHSMHhCkVrtSFMFrrSZKrhKjI 72gC8V/iKCNx8pnMdrOqBjciXuIH3DM0FLsFuUoDSfM8P7kowAqznlb/WlEyFqZKsK4c K2qQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b=CEebtZPX; arc=pass (i=1 spf=pass spfdomain=wesleyan.edu dkim=pass dkdomain=wesleyan.edu dmarc=pass fromdomain=wesleyan.edu); spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.69.112 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu Received: from NAM04-CO1-obe.outbound.protection.outlook.com (mail-eopbgr690112.outbound.protection.outlook.com. [40.107.69.112]) by gmr-mx.google.com with ESMTPS id 3si705691iog.0.2019.11.11.10.26.19 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Nov 2019 10:26:19 -0800 (PST) Received-SPF: pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.69.112 as permitted sender) client-ip=40.107.69.112; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=WEamIwZKkbeUqcGsFZBJFnqaAtsCoiOGrIYX1ZeggfzGPHpyHl4ORLHF0z2Op0r/gsvjvL2W261fZ141hGuu2ElnaNTzz8/lrgk9dbMw/q0cqr9eAObVA/b8SxBTiMGelJRek6ICkm6w69T2X15ifqFMxcP6maDUe2LJkDwZuks427J3ur3J+mdaHFBgEqSrrzw3H4hcP2m46O/2vb5wUiCYxqwUKaOXnAQkjf3YVxmOoGifDEBqsfeNdVK4kYT7yDI3YsEYE05e7CMtt2MYQ9F6peXupoPpUZIOaMFc5F9+pv3XF0n9r3N/PKOjCrO9+Bq83q9dHf8WRbeGlNbj7A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=wXp+qEbA9azP6+APPbVVUVq/9WgH79MMCYtDuta+tlg=; b=NwSG/y0K/4blWIhNFR4sX2dCImOTDAY/ojA138PyDSmlCOvAI+5VJwYGdcYCAFW7mcpiag/nYYohayrxOJkI/ddJQbSjTqWe6Lp1mGrvsNoGY+nrpFR1dna+XoUy9maqCJ4nrjheRTMUEnBDWeYj8DBkeM8cgXuSpaT4EumNuu2m0TwU6A+bXz6KbkpaU95xab0zNZh/RUbjkkq85/ekPFqooJChqPcN1a7YVI0CpYxut/nDsN/2mNY8F06BMAf8JlHdDvpS/9iktiH7Zk0wb2XdW4EGQ9G6CMyA0V04pQj/YUIookUfg+fKK6durPok4u60VGG8ogNY0lKHVRM6ZQ== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=wesleyan.edu; dmarc=pass action=none header.from=wesleyan.edu; dkim=pass header.d=wesleyan.edu; arc=none Received: from BYAPR04MB4597.namprd04.prod.outlook.com (52.135.237.151) by BYAPR04MB5462.namprd04.prod.outlook.com (20.178.48.147) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2430.24; Mon, 11 Nov 2019 18:26:16 +0000 Received: from BYAPR04MB4597.namprd04.prod.outlook.com ([fe80::698c:26e1:9f2d:d294]) by BYAPR04MB4597.namprd04.prod.outlook.com ([fe80::698c:26e1:9f2d:d294%3]) with mapi id 15.20.2430.027; Mon, 11 Nov 2019 18:26:16 +0000 From: "Licata, Dan" To: Stefan Monnier CC: =?iso-8859-1?Q?Mart=EDn_H=F6tzel_Escard=F3?= , Homotopy Type Theory Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Thread-Topic: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Thread-Index: AQHVjNSqGfTVzJ5SoU+8Cb1flwEjBqduvKUAgAqgJgCAAAPDAIAAezwAgAGJ3gCAAd4ggIAADpz9gAkO9wA= Date: Mon, 11 Nov 2019 18:26:16 +0000 Message-ID: <0CC0B8D7-3D66-42AD-A2D7-3B897A432B36@wesleyan.edu> References: In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [24.60.108.192] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: f7c3f04e-c335-46f0-de37-08d766d4a3ec x-ms-traffictypediagnostic: BYAPR04MB5462: x-ms-exchange-purlcount: 1 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:9508; x-forefront-prvs: 0218A015FA x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(4636009)(39850400004)(136003)(366004)(396003)(376002)(346002)(199004)(189003)(5660300002)(71190400001)(71200400001)(486006)(7736002)(305945005)(99286004)(6916009)(14454004)(91956017)(11346002)(66476007)(66946007)(36756003)(54906003)(81166006)(2616005)(476003)(316002)(296002)(81156014)(786003)(446003)(76116006)(186003)(256004)(8676002)(76176011)(66446008)(102836004)(26005)(66556008)(64756008)(6506007)(53546011)(6306002)(66066001)(966005)(6116002)(2906002)(75432002)(3846002)(88552002)(33656002)(4326008)(6436002)(6512007)(6486002)(229853002)(6246003)(478600001)(8936002)(25786009)(86362001);DIR:OUT;SFP:1102;SCL:1;SRVR:BYAPR04MB5462;H:BYAPR04MB4597.namprd04.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX:1; received-spf: None (protection.outlook.com: wesleyan.edu does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: qoSOAOPodSiw5gZjnH/5yU4rLO0bddmqYGQmr6mBnENSKZ0Z+zDusBfxikQIGmS6JVJyyms3022rm2X9Ny+/nfkva+UGDSmo4CAwRSOgd61bStOYtycauMo/fdKUrjdQmpVC4A+tIvFq2NhcGzZPjTJvFLIHI1KvTXPpX+EfKW2nl4Tu0W74AvntF1FfPMwZkxUlcX82l2o9QRW6Mz//NcTEk/iQvNAKjK6rEOvjN1LulwaEUeJhxtTAM5XRl43REoTUQuicrlpP/67aSS9o7Loo9psvDisW/whn8LWIeyXq9Xdla/rMz3fjzp8kWRMfwpdAjFU8nhEqyNPUcw9dWbX6tpSO5eKteOBtyL6jFCTjUSCyPp3BQi03Wq7NUhJO1UBzfRX0PDTqppCVY/NubICTfOqzcsbcgyHniJHpqkVGL6TZ1iCPAY7Oh6Blj5ewZa76R9GA3nOJOljV3IT9ybjvLP5qa+83rJY4Gza7jww= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="UTF-8" Content-ID: <26D97A4F18B7D24BA2BBCDF763039909@namprd04.prod.outlook.com> MIME-Version: 1.0 X-OriginatorOrg: wesleyan.edu X-MS-Exchange-CrossTenant-Network-Message-Id: f7c3f04e-c335-46f0-de37-08d766d4a3ec X-MS-Exchange-CrossTenant-originalarrivaltime: 11 Nov 2019 18:26:16.3785 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: a9fd6c79-6d71-49f3-9111-0c8e591dc3d1 X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: kPHI85lAJ5yg69HU2OnybBgRUpkJq9bsKQDqiBDOaimc9XZicXnLBqnM8r3U1GoVrXe9ZrAP85P/qnwkDj4VIw== X-MS-Exchange-Transport-CrossTenantHeadersStamped: BYAPR04MB5462 X-Original-Sender: dlicata@wesleyan.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b=CEebtZPX; arc=pass (i=1 spf=pass spfdomain=wesleyan.edu dkim=pass dkdomain=wesleyan.edu dmarc=pass fromdomain=wesleyan.edu); spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.69.112 as permitted sender) smtp.mailfrom=dlicata@wesleyan.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: , For inductive families, one thing you can do is to think of them in terms of the translation to parametrized inductive types and identity types, so > data Foo (A : Set) : Set where > bar : Id U A UnaryNat -> Foo A in which case bar applied to the Id U BinaryNat UnaryNat that you get from univalence gives a Foo BinaryNat. A related perspective is to think of some transports as additional constructors for inductive families; see e.g. this approach to inductive families in cubical type theory https://www.cs.cmu.edu/~ecavallo/works/popl19.pdf -Dan > On Nov 5, 2019, at 7:06 PM, Stefan Monnier wrote: > >> 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 > -- 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/0CC0B8D7-3D66-42AD-A2D7-3B897A432B36%40wesleyan.edu.