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.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, 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-ot1-x33e.google.com (mail-ot1-x33e.google.com [IPv6:2607:f8b0:4864:20::33e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e74c5df8 for ; Sun, 2 Jun 2019 21:00:27 +0000 (UTC) Received: by mail-ot1-x33e.google.com with SMTP id n19sf234564ota.14 for ; Sun, 02 Jun 2019 14:00:27 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1559509219; cv=pass; d=google.com; s=arc-20160816; b=MbK6rXk8vOHulwE7udkF5tyN7d1YMCOAOjC8kFoYkaaFrdVj10QnvWi3Z55x3YNxUo NR9slQXuF4vkGy9fshrfTh9Fb9Bbxj/Lbc+4smwgTHy7nYdqBkpaw6O1tJUPkJGmhaaW LAmhSB7nzng5Oq2iQ/5Ip1Ap9CP8jGgjkX8bg31y4ZAy27PWjYuQXiUyB4AaPAJr0Al4 lQyjJjIuhMwgWVdT5gUlDzw1kVDgWUJvtW9gTMJB0dzxxCWpC6b/pYm5kR2+GgNWO+Gh TtRUzaY/ND9EX/nvTvvSSY6GuEkZ4OaB9hj2GAuoE1XzorWc8e+RRewxUksnk1w7gqjn vMTQ== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=llTzf/WtqsN2JQpJM+alNHrMVmEVnzkQn47iV5WY6Co=; b=NGmPTgQNlV6zweEuvdyDxB2BtWjO/bOSdWC3UIyZSmbWxaQEie34MGy1dG4WdmNZFC D1ckrCoejfQHZuSt0W0zGkftOmBgEhXNIrr0bRdHfZfHYpgAu6GFiTvsQH7LF6lJK4B1 4l3g6WMH9Gnfh9K17UDhkoHoFUOhQXxa5ifJJMm3rv0UOvvzowLoQ40N+sFUCgYx9/tC vLNLBSLQTIZNdQkv9q7C/7ADXlszbd92AKrUEmWk0lzNmBXnvILbMeoPZYIwBbL+EH19 tz1fXrq3Ao5UBR+HrMu23N8CShR3GM9MR9ry1uSAeC/TNG/YXoiNrksXY6r5T0zGW8ud KLYA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RxvaIE6U; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::d2e as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=llTzf/WtqsN2JQpJM+alNHrMVmEVnzkQn47iV5WY6Co=; b=tkMfo/3fBjQ5JfFPQjG9ZWDT3h7UI/BVvUiygw6kNlhOnOpVn2aZvhLtQa6JppQUjb kEjyl7i7TIctSmlxXnik/PDmyE/yv+F8hGlscYVqMTXVVoY6f8XtpsIhWd829JsgEP5W SwOYtDn0OcEEeOvSbhZu3sYsqkPjsn2CxvssSWP/nstrrIHNhxxSh9XKcRRVQVOKSYPl OZjgeFXiiRYqqV7FOKLvTxwA/woDVwU1wET8Vqab3bvoi9hondhxqRCHwznbpFAuGqYo CuotxOV9mcaLneVH85DR13PST8vlTp+vXrns/QHaqPIZv+UpUY5HAYGKpz0m06CWhLMA isjw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=llTzf/WtqsN2JQpJM+alNHrMVmEVnzkQn47iV5WY6Co=; b=lAit2NmJYuPkrU1zOKDDeGEpfmDZ/FRohyP/hMvbDSVe+CgG1DtHNs/8XNarSXTiMe c6rHXvEia51dk13ioU1qVsSSDr8AXEYHmHyKTK2V7tm07VCH+JUWmebWxHQt+lzf/dS/ nqtNfRBIcNG1HE/wRSXELEpbvvdFJokfXKlKEKpS8x13NQF60SobLaZREFXxbjJfgmS7 qPwq61l8uZg9iZo36bj7dLtdbCiRn0daCRTHI4+uzpGhn78Ntz9I/2MD02jBVTcs7+/d hv+8AUu4oBTc6MQoDGaxkcHoeWSF5YdACWVA23OZyBmUJp0oDyFMbmvlI7E2rb4+ukq/ vBrw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=llTzf/WtqsN2JQpJM+alNHrMVmEVnzkQn47iV5WY6Co=; b=evfsHC7v/gNyALmsYMmlaiV0nQhdAf0I4FLlXsNW/roeeAp29Uu3Ay5b+LZ6CEMApG 3MN8FsNGrG7RjTy+9WSe4AYnu4vrYxEJn/GclxoLPMQDWLcY+A0cbbyThR+Inj5AJ8bG 3w8OagB2ykeiwZVy8YPPxnaxV7uVNIwMqfu0cFext0wSJuFztv6V2Q7m5Q6BiHS9uZpK 533y9OOSU2+MRoG+NNpUWomUCsdmF4GI6Y6+vFoM0nS45kGaZxl9iFpSOOFgW0ZI4l17 8jcM3Sk70yhsqY3gguKYnPO5X90HwoleoyCl9lVD0mXBvcn33gqPMp8zVR1VszgKtlDm A2xg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWL7ULG3MYZOSaoa3PGtw+3cbnQYE7YIrBR1WNuLQBQmkieSafI DcYF8qVaDpWRe7iJyGdODgM= X-Google-Smtp-Source: APXvYqzvWpcRW7s9hWvs/xw7ymxolJEFB4kO6AIo7umhQ7u766Qp5KXcyeNnQEH/YKge+dpGwQrbQA== X-Received: by 2002:aca:b606:: with SMTP id g6mr5681398oif.101.1559509219528; Sun, 02 Jun 2019 14:00:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:3e45:: with SMTP id h5ls76734otg.11.gmail; Sun, 02 Jun 2019 14:00:18 -0700 (PDT) X-Received: by 2002:a9d:62d4:: with SMTP id z20mr23154otk.340.1559509218300; Sun, 02 Jun 2019 14:00:18 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1559509218; cv=none; d=google.com; s=arc-20160816; b=XfzRIgLNMkkjQwiL2j1W2MgHKbX0S1S78O7OM2rg9xu89YBKDvuuH922J0chKGxiO7 HjK8oKYYaoPgSIP5ah0d9B2uTbnsxVVTkXMLncS1EZU2wlyvOYWpOWa22HVXVMaXh4uA Iyjz3nGoCPjbY/jLL5+kMpGuZ+Sx4eXRvGl5vv0YQGMK9sedYni+oLDutB9UXA0s+fnv 1EVPNzuZKkS8NANr6NElogL0FoqITrHdrzTWk4t8f52fhpsmoBqH2/VUQcM1n/pJ4y3Y St5NwHjAj09pdTVuwJ4mTMHOa2XdfWMrnXiL9H5R19ZzFN2vkJuiAuC7V3gytTFYRCWS WEIg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=LH9yo//X95Cf1Sa8LxDu3JuU73yHV6nSl2O5l4J84VM=; b=IiLTAWsZ/vnC/Jslbw7GV2KYCwkq63YbC0uT+ofzT9O4vUwvvP6tWA592RXXz23RsK 4MCoD9aD/EltZefH9442QeXDJdunoFofqwoEoOH8vRqIlOD5uT8EGATXjayqbxn6t3IC hP9faKT4hsJHj/3P0tGllc8gHnJraYncgFxZbA93yQHV67DncGNH5n7rM5N+Fp2/SKCz tUT8g5N1UVEysoOJ98mXutFo29VImHrPY1J4p3G4hWdryk39nqp0KB6ZxL4F8xRirrjG PtunL8ltHVmfPKfvPuORDZkD2Ll0wsNvBlWlA1u2Em2eA/TX6/ng7VyOtuz5pJIt3VBc iAlg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RxvaIE6U; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::d2e as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-io1-xd2e.google.com (mail-io1-xd2e.google.com. [2607:f8b0:4864:20::d2e]) by gmr-mx.google.com with ESMTPS id r129si606606oib.4.2019.06.02.14.00.18 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 02 Jun 2019 14:00:18 -0700 (PDT) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::d2e as permitted sender) client-ip=2607:f8b0:4864:20::d2e; Received: by mail-io1-xd2e.google.com with SMTP id g16so12641733iom.9 for ; Sun, 02 Jun 2019 14:00:18 -0700 (PDT) X-Received: by 2002:a05:6602:157:: with SMTP id v23mr8081823iot.80.1559509217845; Sun, 02 Jun 2019 14:00:17 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> <29FFF023-0DB7-4E09-8A77-B4F1C2730203@leeds.ac.uk> In-Reply-To: <29FFF023-0DB7-4E09-8A77-B4F1C2730203@leeds.ac.uk> From: Valery Isaev Date: Sun, 2 Jun 2019 23:59:40 +0300 Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Nicola Gambino Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000f42723058a5d889a" X-Original-Sender: valery.isaev@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RxvaIE6U; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::d2e as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --000000000000f42723058a5d889a Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable This brings an old question of what is a canonical isomorphism . To give a simple example in the realm of HoTT, consider isomorphisms between S^1 and S^1. There is a "canonical" isomorphism, the identity, but there are many others. Are they less canonical? You can transport stuff along any of them, so they are not any less canonical from this perspective= . Regards, Valery Isaev =D0=B2=D1=81, 2 =D0=B8=D1=8E=D0=BD. 2019 =D0=B3. =D0=B2 23:47, Nicola Gambi= no : > Hi, > > > On 2 Jun 2019, at 18:55, Kevin Buzzard > wrote: > > > > 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 > DTT/HoTT/UF are canonical isomorphisms, by which I informally mean that > they are definable only by means of the universal properties characterizi= ng > the objects under consideration. > > This is based on the well-known observation that type theories often > describe the free category with a certain kind of structure. > > Perhaps someone for whom it is not 21:45 on a Sunday can turn this > impression into a theorem or correct it. > > If the impression is correct, then HoTT/UF is the half-way house (whose > structural safety is supported by various models of univalence) and the > mathematicians who work informally mixing equality and canonical > isomorphisms are more extreme (and potentially inconsistent). > > With best wishes, > Nicola > > -- > 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/29FFF023-0DB7-4E09-8= A77-B4F1C2730203%40leeds.ac.uk > . > For more options, visit https://groups.google.com/d/optout. > --=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/CAA520fs2MiSPAKkdyhOnqBSdqPw%2BhYCFL-6QRNAjobP-xKTkKA%40= mail.gmail.com. For more options, visit https://groups.google.com/d/optout. --000000000000f42723058a5d889a Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
This brings an old question of=C2=A0what is = a canonical isomorphism. To give a simple example in the realm of HoTT,= consider isomorphisms between S^1 and S^1. There is a "canonical"= ; isomorphism, the identity, but there are many others. Are they less canon= ical? You can transport stuff along any of them, so they are not any less c= anonical from this perspective.

Regards,
Valery Isaev


=D0=B2=D1=81, 2 =D0=B8=D1=8E=D0=BD. 2019 =D0=B3. = =D0=B2 23:47, Nicola Gambino <N= .Gambino@leeds.ac.uk>:
Hi,

> On 2 Jun 2019, at 18:55, Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote= :
>
> There is a subtle difference. HoTT transfers theorems and definitions<= br> > 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.

Perhaps someone for whom it is not 21:45 on a Sunday can turn this impressi= on into a theorem or correct it.

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).=C2=A0

With best wishes,
Nicola

--
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.com/d/msg= id/HomotopyTypeTheory/29FFF023-0DB7-4E09-8A77-B4F1C2730203%40leeds.ac.uk.
For more options, visit
https://groups.google.com/d/optout.

--
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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAA520fs2MiSPAKkdyhOnqBSdqPw%2B= hYCFL-6QRNAjobP-xKTkKA%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--000000000000f42723058a5d889a--