Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: Valery Isaev <valery.isaev@gmail.com>
To: Nicola Gambino <N.Gambino@leeds.ac.uk>
Cc: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] doing "all of pure mathematics" in type theory
Date: Sun, 2 Jun 2019 23:59:40 +0300
Message-ID: <CAA520fs2MiSPAKkdyhOnqBSdqPw+hYCFL-6QRNAjobP-xKTkKA@mail.gmail.com> (raw)
In-Reply-To: <29FFF023-0DB7-4E09-8A77-B4F1C2730203@leeds.ac.uk>

[-- Attachment #1: Type: text/plain, Size: 3100 bytes --]

This brings an old question of what is a canonical isomorphism
<https://mathoverflow.net/questions/19644/what-is-the-definition-of-canonical>.
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


вс, 2 июн. 2019 г. в 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
> > 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 "=" 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 characterizing
> 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-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 "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/CAA520fs2MiSPAKkdyhOnqBSdqPw%2BhYCFL-6QRNAjobP-xKTkKA%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 4504 bytes --]

  reply index

Thread overview: 31+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-05-25 10:12 Kevin Buzzard
2019-05-25 10:22 ` Steve Awodey
2019-05-25 12:23   ` Kevin Buzzard
     [not found]   ` <B7D67BBA-5E0B-4438-908D-4EF316C8C1F1@chalmers.se>
     [not found]     ` <CAH52Xb1Y=Xq=012v_-KSDUuwgnKpEp5qjrxgtUJf+qc_0RWJUg@mail.gmail.com>
2019-05-25 13:13       ` Fwd: " Kevin Buzzard
2019-05-25 13:34   ` Juan Ospina
2019-05-25 14:50     ` Noah Snyder
2019-05-25 15:36       ` Kevin Buzzard
2019-05-25 16:41         ` Noah Snyder
2019-05-26  5:50           ` Bas Spitters
2019-05-26 11:41             ` Kevin Buzzard
2019-05-26 12:09               ` Bas Spitters
2019-05-26 17:00                 ` Kevin Buzzard
2019-05-27  2:33                   ` Daniel R. Grayson
2019-06-02 16:30                   ` Bas Spitters
2019-06-02 17:55                     ` Kevin Buzzard
2019-06-02 20:46                       ` Nicola Gambino
2019-06-02 20:59                         ` Valery Isaev [this message]
2019-06-04 20:32                       ` Michael Shulman
2019-06-04 20:58                         ` Kevin Buzzard
2019-06-06 16:30                         ` Matt Oliveri
2019-05-27 13:09                 ` Assia Mahboubi
2019-05-28  9:50                   ` Michael Shulman
2019-05-28 10:13                     ` Nils Anders Danielsson
2019-05-28 10:22                       ` Michael Shulman
2019-05-29 19:04                         ` Martín Hötzel Escardó
2019-05-30 17:14                           ` Michael Shulman
2019-06-02 17:49                             ` Kevin Buzzard
2019-06-04 20:50                               ` Martín Hötzel Escardó
2019-06-05 17:11                                 ` Thorsten Altenkirch
2019-05-28 15:20                     ` Joyal, André
2019-05-27  8:41           ` Nils Anders Danielsson

Reply instructions:

You may reply publically to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=CAA520fs2MiSPAKkdyhOnqBSdqPw+hYCFL-6QRNAjobP-xKTkKA@mail.gmail.com \
    --to=valery.isaev@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=N.Gambino@leeds.ac.uk \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox