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=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-lf1-x13e.google.com (mail-lf1-x13e.google.com [IPv6:2a00:1450:4864:20::13e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 203ad208 for ; Sun, 2 Jun 2019 20:47:15 +0000 (UTC) Received: by mail-lf1-x13e.google.com with SMTP id j27sf440786lfh.4 for ; Sun, 02 Jun 2019 13:47:14 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1559508434; cv=pass; d=google.com; s=arc-20160816; b=FGxfWVeY8wz4XpGFgnvc1yUkx1svHET1LDE/CKcogvhkwgT3FPPEo9R1dAKCZ9Qa3y 6fowpeqJep8PFSa84IjSwsErc7gmNRQHOleLHGUiL+/0e+w/Ai9oRbH5UqZJS1WEVuGs uamYWi9rtEiBv3l4/PcHxfP/KZJxTVH/+yket6GVEWf9ENwiJo0PUxScSZNUYe6Wc34J f1jfBO3XpvGFZsf1QQmXFU72H616RJLoVOKKvyntA/hDOmsYvXAXlHpZ7pSjQp42T6Fp m4LzTcQrW3eOJU9LGCZM7oEZzfLd6ux8zZYN5aLDfG8eiICoSSv9toZ+5gEaAgAEInCp srIA== 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:content-transfer-encoding :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=K7IuCGUno/JnCAJB3yoUdMIWbicWX6c8a5lJ/91z/JE=; b=Utvya50KM11+KFbPb4lqK+ju/UopXkH8JcUqGg939DSEQLpaI/0A2B9GwN2ptV6NGy vPtxsmPG2gcAhFFOnKCSl52U87B0sZR/+pC4Ww9qZyUQ2Y2IuWHbjX23kfUlML4nrloh QYDUReIfAflHiRzW1PRIDXC531hvDeGPhS0p1Wd9Q6NwDwfoaYkLqwYLvYq3/gKjbxBz S/tBmbD9X8/ToeSPld/OWcZ7nLVA80Y9tkRpqg/xYJPBWWT32Ei8r6EpStNvu+OyjL8D uXQqYHHZpAJhlLCXzW6M4oiu2sxKsoN+JZwoPO/ad/4XlkSiYJlWVZ6/iHJkOF3VvVAZ d/Rw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@leeds365.onmicrosoft.com header.s=selector1-leeds365-onmicrosoft-com header.b=BU5RS19I; spf=pass (google.com: domain of n.gambino@leeds.ac.uk designates 129.11.76.154 as permitted sender) smtp.mailfrom=N.Gambino@leeds.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=leeds.ac.uk 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 :content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=K7IuCGUno/JnCAJB3yoUdMIWbicWX6c8a5lJ/91z/JE=; b=HRfI1WRG/4pEV1QIqkn2NTVKbndxI0qjz5K5lx9jo2pw31hly1mVu8JnVjZSJIgfSy 0eD9hsg/o/10p/Gb0o7mFRo5QyZ04fPOwwd2tDUzg0qM+tzFKdk1++Qf5DU6JSaI8bar tTeEZRm6oQ5KPjsS+bVS+09R2276dXFC7VwYMXRkWwHYH6cJjrBM7l9Fuz3624xjMjyt H4LrvVIahlIHf9y//dqeg0VsXd8JU2J2sgGAjUa0Fax+oG0KDjbgRUH8FJMq6K8IIeJ6 AVl94VYasbh2JIvDka/DHYleX38PDd16nFJ7U+53K4Pa+fb2Paf5fP24Sbuu5G/8MH69 Qr1g== 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:content-transfer-encoding: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=K7IuCGUno/JnCAJB3yoUdMIWbicWX6c8a5lJ/91z/JE=; b=ic3adr8se0LGgfoPuwbtVdesA+bVqwk13sCksoqrjAod0TuVZtrz26Fa3FDsxYQIMB Pt6x91haWrfGJ8dvDY92en/CbthWnDN9GQOptnj2EnBqeNWnONx9anMv1zHtfuQhFyU3 XFOUPeIZ5L/mXjjjs+vYznMzbCL5XN97Ei3c6Ho/FbiVCUefZOuBGLBxxkO8633KzLnB bIGI0aursphd18JbK0aLKlwjcjyAPt+5AHJX2/D5MJuo5Ec3BvWH9z19H0fxsHlfPtEG Q0u0jypo04AF1Ml9OOsIVvVKP/A8XpQqMipAwEoM9YwNcV2kfRFUASGNCMet6Nm3Hfk0 ia6A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAW4QQkPeSQL3DsKWWAiqzqoo7iZgQVWbkwuRAQthM5GxAPE1qL0 PJ/TnXIJtqiYyrhiS0lMzPg= X-Google-Smtp-Source: APXvYqwGHQsJ/q1SaSyoCTqsSPTCyLAmEpQY2GOU/JiszcUn5StVscb2iIbyVlhKwYGmr2AkY/QPTQ== X-Received: by 2002:a05:6512:24a:: with SMTP id b10mr9592287lfo.37.1559508434458; Sun, 02 Jun 2019 13:47:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:614d:: with SMTP id m13ls1417394lfk.1.gmail; Sun, 02 Jun 2019 13:47:10 -0700 (PDT) X-Received: by 2002:a05:6512:144:: with SMTP id m4mr12029687lfo.114.1559508430086; Sun, 02 Jun 2019 13:47:10 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1559508430; cv=none; d=google.com; s=arc-20160816; b=IN8uJMHQPG0T7D0+wAHXqaQb9K+Ko/mSl17t+tO2yR9x8UO8ffxVybX05U5S1gj+JE W3UEiYp2U7xhc29+fMvuav/drHRA07A1k3PActFiBvzpzurzo8ivithDfnQqFCaiy6bn VrIcpdcTpzNkIM9UKQZ7VmclfgNx7FvQoD7nMpdGb0uViOYTyVhSVS4znUhV6Od/BUQW 2WqGmeJGlTk3oPGBezNFqxtAOP0EtTT0aQIWQVHua8lNCN0MQoW12gjYh2rMwxqaQec5 vARZuSDcokAePDQxhK3EUDA4fnjpJztjL/IIlTKZS319ZLxCmPnzyF6ITSbU3m+b9Ckz gNJQ== ARC-Message-Signature: i=1; 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=LLsclD5xZ+XbForyan+dSorGXGlBAwigFm98QOh+n98=; b=zR3uD+IPSkNIf4WXkO8IIRQvzH/k+1EmWRTRIx9bTAbNrPcRaGwhlV9fF9uHNYV2Cl 16vEonKnBZQq5AYIRU8B4PS3VsHKg6QBqwM6sv7imqB1lNZVS0KxkL1m4pWz6QH07xOW c3eb7VRXfUO44L9ywufsO/UG+y0LWXjk3LsgabgSoVIn+4fh5C+mEFKu3Kg3nZ1v7PiA sUvbwMrlROQWp7qFcjJWmqos1FBShBPuRiouYFZCO7UhlZW2oDri/5jDmTZE+ymKceP5 rfRVzuclrp6O7Ihv38B8yl0zd4TOLCVcC/f3QtLC9D8wX72ez2s03a8jwt0tpZfrsjI1 /uQw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@leeds365.onmicrosoft.com header.s=selector1-leeds365-onmicrosoft-com header.b=BU5RS19I; spf=pass (google.com: domain of n.gambino@leeds.ac.uk designates 129.11.76.154 as permitted sender) smtp.mailfrom=N.Gambino@leeds.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=leeds.ac.uk Received: from mhost02c.leeds.ac.uk (mhost02c.leeds.ac.uk. [129.11.76.154]) by gmr-mx.google.com with ESMTPS id p88si355497lja.5.2019.06.02.13.47.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 02 Jun 2019 13:47:09 -0700 (PDT) Received-SPF: pass (google.com: domain of n.gambino@leeds.ac.uk designates 129.11.76.154 as permitted sender) client-ip=129.11.76.154; Received: from APOLLO1.ds.leeds.ac.uk (apollo1.leeds.ac.uk [129.11.5.4]) by mhost02c.leeds.ac.uk (8.14.4/8.14.4) with ESMTP id x52Kkmm1005769 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NOT); Sun, 2 Jun 2019 21:46:48 +0100 Received: from APOLLO8.ds.leeds.ac.uk (129.11.6.119) by APOLLO1.ds.leeds.ac.uk (129.11.5.4) with Microsoft SMTP Server (TLS) id 8.3.245.1; Sun, 2 Jun 2019 21:46:47 +0100 Received: from EUR04-HE1-obe.outbound.protection.outlook.com (104.47.13.51) by outlook.leeds.ac.uk (129.11.6.119) with Microsoft SMTP Server (TLS) id 14.3.195.1; Sun, 2 Jun 2019 21:46:47 +0100 Received: from DB7PR03MB3641.eurprd03.prod.outlook.com (52.134.98.154) by DB7PR03MB5065.eurprd03.prod.outlook.com (20.178.46.203) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1943.22; Sun, 2 Jun 2019 20:46:45 +0000 Received: from DB7PR03MB3641.eurprd03.prod.outlook.com ([fe80::e8d0:9065:3e82:e41a]) by DB7PR03MB3641.eurprd03.prod.outlook.com ([fe80::e8d0:9065:3e82:e41a%3]) with mapi id 15.20.1943.018; Sun, 2 Jun 2019 20:46:45 +0000 From: Nicola Gambino To: Kevin Buzzard CC: Bas Spitters , Noah Snyder , Homotopy Type Theory , Juan Ospina Subject: Re: [HoTT] doing "all of pure mathematics" in type theory Thread-Topic: [HoTT] doing "all of pure mathematics" in type theory Thread-Index: AQHVEuJWUFc58Ule20C2Tp9JnJ36bKZ7oceAgAA1u4CAABULAIAADOgAgAASRYCAANxQgIAAYg2AgAAH8wCAAFEagIAK9+8AgAAX9oCAAC/FAA== Date: Sun, 2 Jun 2019 20:46:45 +0000 Message-ID: <29FFF023-0DB7-4E09-8A77-B4F1C2730203@leeds.ac.uk> References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> In-Reply-To: Accept-Language: en-GB, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-mailer: Apple Mail (2.3445.9.1) x-originating-ip: [95.150.86.78] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 7d303ec4-43f4-49cf-ba8f-08d6e79b6d0f x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600148)(711020)(4605104)(1401327)(2017052603328)(7193020);SRVR:DB7PR03MB5065; x-ms-traffictypediagnostic: DB7PR03MB5065: x-ms-exchange-purlcount: 1 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:8882; x-forefront-prvs: 005671E15D x-forefront-antispam-report: SFV:NSPM;SFS:(10009020)(346002)(376002)(136003)(366004)(396003)(39860400002)(189003)(199004)(5660300002)(6512007)(6486002)(256004)(6306002)(66446008)(64756008)(66476007)(66946007)(66556008)(66066001)(91956017)(76116006)(6916009)(73956011)(25786009)(6116002)(478600001)(76176011)(3846002)(54906003)(966005)(81156014)(81166006)(6246003)(14454004)(7736002)(305945005)(186003)(72206003)(786003)(8676002)(316002)(6436002)(53936002)(99286004)(2906002)(4326008)(57306001)(6506007)(53546011)(50226002)(83716004)(86362001)(82746002)(446003)(71200400001)(71190400001)(33656002)(26005)(102836004)(11346002)(486006)(2616005)(36756003)(476003)(74482002)(8936002)(68736007)(229853002);DIR:OUT;SFP:1101;SCL:1;SRVR:DB7PR03MB5065;H:DB7PR03MB3641.eurprd03.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; received-spf: None (protection.outlook.com: leeds.ac.uk does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: D+WTbt+1NqvhuDXry3xFFoNKXyBS2qipUdnFx3Qh+DU3HmX4ULLISL5QEVZognPDtOBpEejiwYKkE2HCm/Yyx8Np3HmqymaT8aFsdixUhONVHKpdtaMqv7eVUyMBkTfTLQ7dH/6F8blb8a9vi5lYqb1+RXVrAxmSZ8fjk0JFTReN6cukQDuTOZb/B5KCoiukxw5o432UuEaQ6doTCXaLBfR/wPtv0oiwfBYMgFHDdTJGEs1jilQ4AFhQiQWPzmzvjBiWBPiKtq9ZMAOYlYpL6/L6AfOZrRABVfUNJq+b+JqV56DL9iRrjUAE52Fj+hL3kR6e1lk7W/u5G75ffNMw9jLRnFGOnMPYQ2ryojcMVPe1mEea4gVciJ6jWM8PcyjD5bfknEsGGnj3f3TmjlW4ChtFIwYxQ6a7DRTYdVcI5+I= Content-Type: text/plain; charset="UTF-8" Content-ID: <12E2D153CAD7004185DBB090799EC34E@eurprd03.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 7d303ec4-43f4-49cf-ba8f-08d6e79b6d0f X-MS-Exchange-CrossTenant-originalarrivaltime: 02 Jun 2019 20:46:45.3929 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: bdeaeda8-c81d-45ce-863e-5232a535b7cb X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: pmtng@leeds.ac.uk X-MS-Exchange-Transport-CrossTenantHeadersStamped: DB7PR03MB5065 X-OriginatorOrg: leeds.ac.uk X-UOL-RateLimit: userRateLimit[a:n.gambino@leeds.ac.uk,c:0.6237431488893215,l:500.0] X-Original-Sender: n.gambino@leeds.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@leeds365.onmicrosoft.com header.s=selector1-leeds365-onmicrosoft-com header.b=BU5RS19I; spf=pass (google.com: domain of n.gambino@leeds.ac.uk designates 129.11.76.154 as permitted sender) smtp.mailfrom=N.Gambino@leeds.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=leeds.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: , Hi, > On 2 Jun 2019, at 18:55, Kevin Buzzard wrote: >=20 > There is a subtle difference. HoTT transfers theorems and definitions > across all isomorphisms. In the definition of a scheme, the stacks > project transfers an exact sequence along a *canonical isomorphism*. > Canonical isomorphism is denoted by "=3D" in some literature (e.g. see > some recent tweets by David Roberts like > https://twitter.com/HigherGeometer/status/1133993485034332161). This > is some sort of weird half-way house, not as extreme as HoTT, not as > weak as DTT, but some sort of weird half-way house where > mathematicians claim to operate; this is an attitude which is > beginning to scare me a little. I am under the impression that all isomorphisms that are definable within D= TT/HoTT/UF are canonical isomorphisms, by which I informally mean that they= are definable only by means of the universal properties characterizing the= objects under consideration. This is based on the well-known observation that type theories often descri= be the free category with a certain kind of structure.=20 Perhaps someone for whom it is not 21:45 on a Sunday can turn this impressi= on into a theorem or correct it.=20 If the impression is correct, then HoTT/UF is the half-way house (whose str= uctural safety is supported by various models of univalence) and the mathem= aticians who work informally mixing equality and canonical isomorphisms are= more extreme (and potentially inconsistent). =20 With best wishes, Nicola --=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/29FFF023-0DB7-4E09-8A77-B4F1C2730203%40leeds.ac.uk. For more options, visit https://groups.google.com/d/optout.