Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: Nicola Gambino <N.Gambino@leeds.ac.uk>
To: Kevin Buzzard <kevin.m.buzzard@gmail.com>
Cc: Bas Spitters <b.a.w.spitters@gmail.com>,
	Noah Snyder <nsnyder@gmail.com>,
	Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>,
	Juan Ospina <jospina65@gmail.com>
Subject: Re: [HoTT] doing "all of pure mathematics" in type theory
Date: Sun, 2 Jun 2019 20:46:45 +0000
Message-ID: <29FFF023-0DB7-4E09-8A77-B4F1C2730203@leeds.ac.uk> (raw)
In-Reply-To: <CAH52Xb0XD3F9=Xc2eHZDAyFHQ-3e+HUXc7kRTp_+vhzBPVx-8g@mail.gmail.com>

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.

  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 [this message]
2019-06-02 20:59                         ` Valery Isaev
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=29FFF023-0DB7-4E09-8A77-B4F1C2730203@leeds.ac.uk \
    --to=n.gambino@leeds.ac.uk \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=b.a.w.spitters@gmail.com \
    --cc=jospina65@gmail.com \
    --cc=kevin.m.buzzard@gmail.com \
    --cc=nsnyder@gmail.com \
    /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