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.8 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x538.google.com (mail-ed1-x538.google.com [IPv6:2a00:1450:4864:20::538]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 10f59ca3 for ; Wed, 27 Nov 2019 10:12:43 +0000 (UTC) Received: by mail-ed1-x538.google.com with SMTP id j3sf13006472edt.7 for ; Wed, 27 Nov 2019 02:12:43 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language: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=Hw1+9BLLUo1Eed17ZU84g0WpClo2nvjCHDycB1ymzUs=; b=OlU0EaQN12GH6ckfOBiVmIX8JSEvc0cuXcpJ7qTb+CIuns8+6TwtDxBv8/aAeDsVES xjAbNixRzwIH4auGmqgE4QXj3la0epA21pAgDbmyWWkevlsuXDbtzVz3SWU3eN20ozVq 7GNfAPpBl6uesiZlCXxWBfGLFDdVQW6YQoSrU8/iGwauGgTQTNrnqb8mpPNdVwb1kLr0 muAuN3y3DYLccYejpQKNdDCEEW2hcqYcDDWSk8pdR0mcDNfhGgSEkhXcdGXlZI6kDm1h LTq3QiP4GyUkdacfXMcbGndMhx1PeX6VLBMNU5ZjFeE4BkXgE28/3zHUzlATRAh33+MO hYyw== 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:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language: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=Hw1+9BLLUo1Eed17ZU84g0WpClo2nvjCHDycB1ymzUs=; b=KsEmTq940OO4wYJnhA13jmo5g83MeR8Kre48RM8r0ZJYg/SfjEib+OL5QZQjtuQ/Y/ 4IziJDAQQGto4Jg5ZmrUzlsX6oeXA2VaQ5Xq5zZx0BMtErxR4K7UYMuTSlmgsh8kgj0I Ina2AFfGGo5zIKt4nhICQrgIFaVFxPSyKI5L7V96YwK1mf9sL95trbLN0sVgVGl1pS9O G5mQQWRQmnBZ7o1auFkZZeRvw3f9b4IwZaGCFtpPlCJC/fH7vUxo+CJ5M+ejvSVxr5Ey +BpZpusC3KEMmX3l6bkAOqrph70v6qnj6qiX3EP+QIrclsKcBkRGj5mp1Mqlm/OtIx42 BRYw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXRxGn63bJ5aYsG9TaXC0jhYGjW9ZlG4c3pYOmRfVS++i3so7er dJu6lhSZX3hbPxtbQ1wlZSE= X-Google-Smtp-Source: APXvYqwsy/kQOxlWakCc6gZxwf5lUFZ9wVe+F5fZ2L57iS6q7qhxdeq6OPBMqHaipWin+/oP4kDNfA== X-Received: by 2002:a50:fa4a:: with SMTP id c10mr30491851edq.51.1574849563200; Wed, 27 Nov 2019 02:12:43 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:80ca:: with SMTP id a10ls7263410ejx.0.gmail; Wed, 27 Nov 2019 02:12:42 -0800 (PST) X-Received: by 2002:a17:906:90b:: with SMTP id i11mr49181935ejd.109.1574849562488; Wed, 27 Nov 2019 02:12:42 -0800 (PST) Received: from uidappmx05.nottingham.ac.uk (uidappmx05.nottingham.ac.uk. [128.243.43.128]) by gmr-mx.google.com with ESMTPS id x16si606210eds.5.2019.11.27.02.12.42 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 27 Nov 2019 02:12:42 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) client-ip=128.243.43.128; Received: from uidappmx05.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 2A5A66CF0EB_DDE4C1AB for ; Wed, 27 Nov 2019 10:12:42 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx05.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id 939D06CF0C2_DDE4C19F for ; Wed, 27 Nov 2019 10:12:41 +0000 (GMT) Received: from uiwexedg02.ad.nottingham.ac.uk ([10.159.172.14]) by smtp4.nottingham.ac.uk with esmtp (Exim 4.85) (envelope-from ) id 1iZuJN-0002PB-Hs; Wed, 27 Nov 2019 10:12:41 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Wed, 27 Nov 2019 10:12:41 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1531.3; Wed, 27 Nov 2019 10:12:40 +0000 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.13) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Wed, 27 Nov 2019 10:12:40 +0000 Received: from EUR03-VE1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Wed, 27 Nov 2019 10:12:40 +0000 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=YCLw2yzR/dZjNNWMaFWXdltLCGAHdPi5y24+nuTpYw+GeglyJfGXPa4qMvk66YDbK8t9Kdex9fQo8B7VQ8CPG0Z6s9EG55BVMAY6dohu7/uU89WogpafL/qR2muUODRYjA/GfVETcC+2btjbSdB2MU577AvRXHY7EWK0N0ZIREt8ViQwnMlGE+DsxhvKE1AI0dDTjtHAPyiuAcEyvN4s+tNQ8qkvq0+rOG+oB5wTDPQusvPh3PT/sqZpAdNZm/shm6VBGVqVVY5ACS+TUyMrj0nCmcHCwkX7x2VGJcc4tNW/7txUNdIVTYzwCWV88ABzYG8PE/7gNeC3Yo+wcyhi5w== 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=u9hOUMeL9maUdkBaZ4reh19srQYtjh+4VUKALkkqKYo=; b=ctzxGkw+LoAyGY1yjUO2Pp3L8J7tyUgduNMuysfJL5pUjQDUjv8tOsmbiKXzLT0QfPeA2xeELoDoAv7Vlh55LbiRWD+QZZtk5cNEHy2h/MTkiPPZzPocMSAybT4R5rmhs6Z8yQ8GcbVDW0kG13NWzojrNosq0vHNcMTg0oe9w8OZsgbaKaJdwtTH4w/yclpMykkV93uw4MTN48c6yB8DwxH6BKg9mV1GxnhhTOMgCc2bbtG161o7c0/TsrHFkeOk9f5W+i1f7/L5mfqMga3exCMtly3DUeTpYmcHnqzpfvTE1YV9OitKebpATCmrfxlBeKWwoGJs5EkYv/V0Q5F7dg== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=exmail.nottingham.ac.uk; dmarc=pass action=none header.from=exmail.nottingham.ac.uk; dkim=pass header.d=exmail.nottingham.ac.uk; arc=none Received: from AM0PR06MB4020.eurprd06.prod.outlook.com (52.133.59.23) by AM0PR06MB5089.eurprd06.prod.outlook.com (20.178.18.84) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2495.18; Wed, 27 Nov 2019 10:12:39 +0000 Received: from AM0PR06MB4020.eurprd06.prod.outlook.com ([fe80::cc8c:82e0:e69f:e57b]) by AM0PR06MB4020.eurprd06.prod.outlook.com ([fe80::cc8c:82e0:e69f:e57b%7]) with mapi id 15.20.2474.023; Wed, 27 Nov 2019 10:12:39 +0000 From: Thorsten Altenkirch To: =?utf-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , 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: AQHVjNSuJG58LGMm9kupogTuj/cz96duvKUAgAqgJgCAAAPDAIAAezwAgAAJJoCAACwEgIABomcAgB8YCYCAAfrtAIABO4eAgAD64gA= Date: Wed, 27 Nov 2019 10:12:39 +0000 Message-ID: References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> <13f496d9-1d01-4a2f-b5c1-826dd87aebf2@googlegroups.com> In-Reply-To: <13f496d9-1d01-4a2f-b5c1-826dd87aebf2@googlegroups.com> Accept-Language: en-US Content-Language: en-GB X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.1e.0.191013 x-originating-ip: [128.243.2.24] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: b15a8bfc-7df1-42fc-fb58-08d77322557f x-ms-traffictypediagnostic: AM0PR06MB5089: x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:10000; x-forefront-prvs: 023495660C x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(136003)(346002)(39860400002)(366004)(376002)(396003)(199004)(189003)(256004)(186003)(446003)(11346002)(14444005)(478600001)(71190400001)(71200400001)(66446008)(36756003)(2906002)(25786009)(64756008)(66556008)(66476007)(66946007)(76116006)(91956017)(8676002)(7736002)(81156014)(8936002)(5660300002)(86362001)(33656002)(236005)(316002)(54896002)(6306002)(81166006)(66574012)(9686003)(6512007)(229853002)(102836004)(53546011)(6506007)(786003)(6246003)(26005)(966005)(6436002)(606006)(14454004)(66066001)(790700001)(6116002)(3846002)(6486002)(76176011)(110136005)(58126008)(99286004);DIR:OUT;SFP:1102;SCL:1;SRVR:AM0PR06MB5089;H:AM0PR06MB4020.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: WbU7RIN2AA+dZ7KPat2w/yfORAshM1T1TDep0yVosntfqX5bTQgXXpQeaRPhQ/nGAB4w0Dq9xbdIXafaSKPnrC02hKeEK0uKRRxZrgW8hG/hI7wYWOe4sw97zYb7147Sib3g/98PyWbxURE9tqJ15fNAr2/7AzpODtmv9GELcdRocS2+jU/bXHu3Kc5GcOEnBGCCFo1IvItng3t4pzA/0+uRu+X8EK6TOIemdMPeNXaXIwU5F7FzjMG0LT+DKoG7QThvjCHLvsQ85pNp4jgTxV9TbysEcldqb/05871nR9t+CR/Y1JeN/4J6FSIVzKSvBzkT2Jke6gRf+Ca5nZUKygQm+460cEjOZhu4jxgUBWExunozu6V2YdlSy98P+2C+mGur+4lhm6Dlp34woy9T7pCHRyk+pHn7RNuIUO5IILstqoWuGq3wW0qHIb1saGJ1AClLDJDv/L+7Hex0iRdQ8UvEdnBL7F46RDHt3kP94FU= x-ms-exchange-transport-forked: True Content-Type: multipart/alternative; boundary="_000_F89C978666614F12951D3D58B1D71C6Enottinghamacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: b15a8bfc-7df1-42fc-fb58-08d77322557f X-MS-Exchange-CrossTenant-originalarrivaltime: 27 Nov 2019 10:12:39.5148 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: BdHUI/umftxfP2txDsd5t6++e9DSH2hQsGA8MPNSARmiURj11BQCashU0It44b/LFy6kt/4bWN2Zsy60NQVVC7QIOMrQsaROKturVZeVu5F7PeL3wUoGj2k889luFwHp X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM0PR06MB5089 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; arc=fail (body hash mismatch); spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk 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: , --_000_F89C978666614F12951D3D58B1D71C6Enottinghamacuk_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable So writing "x =3D y" for the identity type is a bit perverse. People may say, and they have said "but there is no other sensible notion of equality for such type theories. That may be so, but because, in any case, *it is not the same notion of equality*, we should not use the same symbol. Two mathematical objects are equal if they have the same properties. This i= s exactly what equals means in HoTT and hence we should use the same symbol= and call it equality. Everything else is confusing especially for the newc= omer: =E2=80=9Cwe have something in HoTT which is basically equality but we= call it by a different name and we use a different symbol=E2=80=9D??? Yes, it is different because equality of structures is not a proposition bu= t a structure. But to insist that equality of structure is a proposition is= just a confusion of conventional Mathematics. Independent of conventional Mathematics there is something like a na=C3=AFv= e idea of equality which is preformal. And equality in HoTT is just a way t= o make this preformal notion precise. And why is it so strange to say there= is more than one way to objects can be equal? As far is the notion of =E2=80=9Ccanonical isomorphism=E2=80=9D, Kevin is i= nterested in, is concerned, I think this is an intensional aspect of an equ= ality and hence not expressible within HoTT. E.g. 3+4 and 7 are the same na= tural number but 7 is canonical. Thorsten From: on behalf of Mart=C3=ADn H=C3= =B6tzel Escard=C3=B3 Date: Tuesday, 26 November 2019 at 19:15 To: Homotopy Type Theory Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be = 'impractical'? On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: HoTT instead expands the notion of "equality" to essentially mean "isomorphism" and requires transporting along it as a nontrivial action. I doubt that that's what you have in mind, but maybe you could explain what you do mean? I think terminology and notation alone cause a lot of confusion (and I have said this many times in this list in the past, before Kevin joined in)= . Much of the disagreement is not a real disagreement but a misunderstanding. * In HoTT, or in univalent mathematics, we use the terminology "equals" and the notation "=3D" for something that is not the same notion as in "traditional mathematics". * Before the univalence axiom, we had Martin-Loef's identity type. * It was *intended* to capture equality *as used by mathematicians* (constructive or not). * But it didn't. Hofmann and Streicher proved that. * The identity type captures something else. It certainly doesn't capture truth-valued equality by default. In particular, Voevosdky showed that it captures isomorphism of sets, and more generality equivalence of =E2=88=9E-groupoids. But this is distorting history a bit. In the initial drafts of his "homotopy lambda calculus", he tried come up with a new construction in type theory to capture equivalence. It was only later that he found out that what he needed was precisely Martin-Loef's identity type. * So writing "x =3D y" for the identity type is a bit perverse. People may say, and they have said "but there is no other sensible notion of equality for such type theories. That may be so, but because, in any case, *it is not the same notion of equality*, we should not use the same symbol. * Similarly, writing "X =E2=89=83 Y" is a bit perverse, too. In truth-valued mathematics, "X =E2=89=83 Y" is most of the time intende= d to be truth-valued, not set-valued. (Exception: category theory. E.g. we write a long chain of isomorphisms to establish that two objects are isomorphic. Then we learn that the author of such a proof was not interested in the existence of an isomorphism, but instead to provide an example. Such a proof/construction is usually concluded by saying something like "by chasing the isomorphism, we see that we can take [...] as our desired isomorphism.) * With the above out of the way, we can consider the imprecise slogan "isomorphic types are equal". The one thing that the univalence axiom doesn't say is that isomorphic type are equal. What it does say is that the *identity type* Id X Y is in canonical bijection with the type X =E2=89=83 Y of equivalences. * What is the effect of this? - That the identity type behaves like isomorphism, rather than like equality. - And that isomorphism behaves a little bit like equality. The important thing above is "a little bit". In particular, we cannot *substitute* things by isomorphic things. We can only *transport* them (just like things work as usual with isomorphisms). * Usually, the univalence axioms is expressed as a relation between equality and isomorphism. Where by equality we don't mean equality but instead the identity type. A way to avoid these terminological problems is to formulate univalence as a property of isomorphisms, or more precisely equivalences. To show that all equivalences satisfy a given property, it is enough to prove that all the identity equivalence between any two types have this property. * So, as Mike says above, most of the time we can work with type equivalence rather than "type equality". And I do too. Something that is not well explained at all in the literature is when and how the univalence axiom *actually makes a difference*. (I guess this is not well understood. I used to thing that the univalence axioms makes a difference only for types that are not sets. But actually, for example, the univalence axiom is needed (in the absence of the K axiom) to prove that the type of ordinals is a set.) * One example: object classifiers, subtype classifiers, ... * Sometimes the univalence axiom may be *convenient* but *not needed*. I guess that Kevin is, in particular, saying precisely that. In all cases where he needs to transport constructions along isomorphisms, he is confident that this can be done without univalence. And I would agree with this assessment. Best, Martin -- 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/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com<= https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c= 1-826dd87aebf2%40googlegroups.com?utm_medium=3Demail&utm_source=3Dfooter>. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment.=20 Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored=20 where permitted by law. --=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/F89C9786-6661-4F12-951D-3D58B1D71C6E%40nottingham.ac.uk. --_000_F89C978666614F12951D3D58B1D71C6Enottinghamacuk_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable

So writing "x =3D = y" for the identity type is a bit perverse.

 

   People may= say, and they have said "but there is no other sensible

   notion of = equality for such type theories.

 

   That may b= e so, but because, in any case, *it is not the same

   notion of = equality*, we should not use the same symbol.

 

Two mathematical objects are equal if they have the = same properties. This is exactly what equals means in HoTT and hence we sho= uld use the same symbol and call it equality. Everything else is confusing especially for the newcomer: =E2=80=9Cwe have= something in HoTT which is basically equality but we call it by a differen= t name and we use a different symbol=E2=80=9D???

 

Yes, it is different because equality of structures = is not a proposition but a structure. But to insist that equality of struct= ure is a proposition is just a confusion of conventional Mathematics.

 

Independent of conventional Mathematics there is som= ething like a na=C3=AFve idea of equality which is preformal. And equality = in HoTT is just a way to make this preformal notion precise. And why is it so strange to say there is more than one way to obj= ects can be equal?

 

As far is the notion of =E2=80=9Ccanonical isomorphi= sm=E2=80=9D, Kevin is interested in, is concerned, I think this is an inten= sional aspect of an equality and hence not expressible within HoTT. E.g. 3+4 and 7 are the same natural number but 7 is canonical.

 

Thorsten

 

 

 

&nbs= p;

&nbs= p;

From= : <homotopytypet= heory@googlegroups.com> on behalf of Mart=C3=ADn H=C3=B6tzel Escard=C3= =B3 <escardo.martin@gmail.com>
Date: Tuesday, 26 November 2019 at 19:15
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>=
Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants= to be 'impractical'?

 



On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote:

HoTT instead expands the notion of "equality&qu= ot; to
essentially mean "isomorphism" and requires transporting along it= as a
nontrivial action.  I doubt that that's what you have in mind, but maybe you could explain what you do mean?

 

 I think terminology and notation alone cause a= lot of confusion (and I

have said this many times in this list in the past, = before Kevin joined in).

 

Much of the disagreement is not a real disagreement = but a

misunderstanding.

 

 * In HoTT, or in univalent mathematics, we use= the terminology

   "equals" and the notation &qu= ot;=3D" for something that is not the same

   notion as in "traditional mathemat= ics".

 

 * Before the univalence axiom, we had Martin-L= oef's identity type.

 

 * It was *intended* to capture equality *as us= ed by mathematicians*

   (constructive or not).

 

 * But it didn't. Hofmann and Streicher proved = that.

 

 * The identity type captures something else.

 

   It certainly doesn't capture truth-valu= ed equality by default.

 

   In particular, Voevosdky showed that it= captures isomorphism of

   sets, and more generality equivalence o= f =E2=88=9E-groupoids.

 

   But this is distorting history a bit.

 

   In the initial drafts of his "homo= topy lambda calculus", he tried

   come up with a new construction in type= theory to capture

   equivalence.

 

   It was only later that he found out tha= t what he needed was

   precisely Martin-Loef's identity type.<= o:p>

 

 * So writing "x =3D y" for the ident= ity type is a bit perverse.

 

   People may say, and they have said &quo= t;but there is no other sensible

   notion of equality for such type theori= es.

 

   That may be so, but because, in any cas= e, *it is not the same

   notion of equality*, we should not use = the same symbol.

 

 * Similarly, writing "X =E2=89=83 Y" is a bit perverse, too.

 

   In truth-valued mathematics, "X =E2=89=83 Y" is most of the time intended

   to be truth-valued, not set-valued.

 

   (Exception: category theory. E.g. we wr= ite a long chain of

   isomorphisms to establish that two obje= cts are isomorphic. Then we

   learn that the author of such a proof w= as not interested in the

   existence of an isomorphism, but instea= d to provide an

   example. Such a proof/construction is u= sually concluded by saying

   something like "by chasing the iso= morphism, we see that we can take

   [...] as our desired isomorphism.)=

 

 

 * With the above out of the way, we can consid= er the imprecise slogan

   "isomorphic types are equal".=

 

   The one thing that the univalence axiom= doesn't say is that

   isomorphic type are equal.

 

   What it does say is that the *identity = type* Id X Y is in canonical

   bijection with the type X =E2=89=83 Y of equivalences.

 

 * What is the effect of this?

 

   - That the identity type behaves like i= somorphism, rather than like

     equality.

 

   - And that isomorphism behaves a little= bit like equality.

 

   The important thing above is "a li= ttle bit".

 

   In particular, we cannot *substitute* t= hings by isomorphic

   things. We can only *transport* them (j= ust like things work as

   usual with isomorphisms).

 

 * Usually, the univalence axioms is expressed = as a relation between

   equality and isomorphism.

 

   Where by equality we don't mean equalit= y but instead the identity

   type.

 

   A way to avoid these terminological pro= blems is to formulate

   univalence as a property of isomorphism= s, or more precisely

   equivalences.

 

   To show that all equivalences satisfy a= given property, it is

   enough to prove that all the identity e= quivalence between any two

   types have this property.

 

 * So, as Mike says above, most of the time we = can work with type

   equivalence rather than "type equa= lity". And I do too.

 

   Something that is not well explained at= all in the literature is

   when and how the univalence axiom *actu= ally makes a difference*.

 

   (I guess this is not well understood. I= used to thing that the

   univalence axioms makes a difference on= ly for types that are not

   sets. But actually, for example, the un= ivalence axiom is needed (in

   the absence of the K axiom) to prove th= at the type of ordinals is a

   set.)

 

      * One example: object classifie= rs, subtype classifiers, ...

 

 * Sometimes the univalence axiom may be *conve= nient* but *not needed*.

 

   I guess that Kevin is, in particular, s= aying precisely that. In all

   cases where he needs to transport const= ructions along isomorphisms,

   he is confident that this can be done w= ithout univalence. And I

   would agree with this assessment.<= /o:p>

 

Best,

Martin

 

 

 

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to Homo= topyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c= 1-826dd87aebf2%40googlegroups.com.


This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.=20

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored=20
where permitted by law.

--
You received this message because you are subscribed to the Google Groups &= quot;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.co= m/d/msgid/HomotopyTypeTheory/F89C9786-6661-4F12-951D-3D58B1D71C6E%40notting= ham.ac.uk.
--_000_F89C978666614F12951D3D58B1D71C6Enottinghamacuk_--