Re: [HoTT] doing "all of pure mathematics" in type theory

[Valery Isaev <valery.isaev@gmail.com>]

[-- 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 --]