From: Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk>
To: "Martín Hötzel Escardó" <escardo.martin@gmail.com>,
"Homotopy Type Theory" <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?
Date: Wed, 27 Nov 2019 10:12:39 +0000 [thread overview]
Message-ID: <F89C9786-6661-4F12-951D-3D58B1D71C6E@nottingham.ac.uk> (raw)
In-Reply-To: <13f496d9-1d01-4a2f-b5c1-826dd87aebf2@googlegroups.com>
[-- Attachment #1: Type: text/plain, Size: 7827 bytes --]
So writing "x = y" for the identity type is a bit perverse.
People may say, and they have said "but there is no other sensible
notion of equality for such type theories.
That may be so, but because, in any case, *it is not the same
notion of equality*, we should not use the same symbol.
Two mathematical objects are equal if they have the same properties. This is exactly what equals means in HoTT and hence we should use the same symbol and call it equality. Everything else is confusing especially for the newcomer: “we have something in HoTT which is basically equality but we call it by a different name and we use a different symbol”???
Yes, it is different because equality of structures is not a proposition but a structure. But to insist that equality of structure is a proposition is just a confusion of conventional Mathematics.
Independent of conventional Mathematics there is something like a naïve idea of equality which is preformal. And equality in HoTT is just a way to make this preformal notion precise. And why is it so strange to say there is more than one way to objects can be equal?
As far is the notion of “canonical isomorphism”, Kevin is interested in, is concerned, I think this is an intensional aspect of an equality and hence not expressible within HoTT. E.g. 3+4 and 7 are the same natural number but 7 is canonical.
Thorsten
From: <homotopytypetheory@googlegroups.com> on behalf of Martín Hötzel Escardó <escardo.martin@gmail.com>
Date: Tuesday, 26 November 2019 at 19:15
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?
On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote:
HoTT instead expands the notion of "equality" to
essentially mean "isomorphism" and requires transporting along it as a
nontrivial action. I doubt that that's what you have in mind, but
maybe you could explain what you do mean?
I think terminology and notation alone cause a lot of confusion (and I
have said this many times in this list in the past, before Kevin joined in).
Much of the disagreement is not a real disagreement but a
misunderstanding.
* In HoTT, or in univalent mathematics, we use the terminology
"equals" and the notation "=" for something that is not the same
notion as in "traditional mathematics".
* Before the univalence axiom, we had Martin-Loef's identity type.
* It was *intended* to capture equality *as used by mathematicians*
(constructive or not).
* But it didn't. Hofmann and Streicher proved that.
* The identity type captures something else.
It certainly doesn't capture truth-valued equality by default.
In particular, Voevosdky showed that it captures isomorphism of
sets, and more generality equivalence of ∞-groupoids.
But this is distorting history a bit.
In the initial drafts of his "homotopy lambda calculus", he tried
come up with a new construction in type theory to capture
equivalence.
It was only later that he found out that what he needed was
precisely Martin-Loef's identity type.
* So writing "x = y" for the identity type is a bit perverse.
People may say, and they have said "but there is no other sensible
notion of equality for such type theories.
That may be so, but because, in any case, *it is not the same
notion of equality*, we should not use the same symbol.
* Similarly, writing "X ≃ Y" is a bit perverse, too.
In truth-valued mathematics, "X ≃ Y" is most of the time intended
to be truth-valued, not set-valued.
(Exception: category theory. E.g. we write a long chain of
isomorphisms to establish that two objects are isomorphic. Then we
learn that the author of such a proof was not interested in the
existence of an isomorphism, but instead to provide an
example. Such a proof/construction is usually concluded by saying
something like "by chasing the isomorphism, we see that we can take
[...] as our desired isomorphism.)
* With the above out of the way, we can consider the imprecise slogan
"isomorphic types are equal".
The one thing that the univalence axiom doesn't say is that
isomorphic type are equal.
What it does say is that the *identity type* Id X Y is in canonical
bijection with the type X ≃ Y of equivalences.
* What is the effect of this?
- That the identity type behaves like isomorphism, rather than like
equality.
- And that isomorphism behaves a little bit like equality.
The important thing above is "a little bit".
In particular, we cannot *substitute* things by isomorphic
things. We can only *transport* them (just like things work as
usual with isomorphisms).
* Usually, the univalence axioms is expressed as a relation between
equality and isomorphism.
Where by equality we don't mean equality but instead the identity
type.
A way to avoid these terminological problems is to formulate
univalence as a property of isomorphisms, or more precisely
equivalences.
To show that all equivalences satisfy a given property, it is
enough to prove that all the identity equivalence between any two
types have this property.
* So, as Mike says above, most of the time we can work with type
equivalence rather than "type equality". And I do too.
Something that is not well explained at all in the literature is
when and how the univalence axiom *actually makes a difference*.
(I guess this is not well understood. I used to thing that the
univalence axioms makes a difference only for types that are not
sets. But actually, for example, the univalence axiom is needed (in
the absence of the K axiom) to prove that the type of ordinals is a
set.)
* One example: object classifiers, subtype classifiers, ...
* Sometimes the univalence axiom may be *convenient* but *not needed*.
I guess that Kevin is, in particular, saying precisely that. In all
cases where he needs to transport constructions along isomorphisms,
he is confident that this can be done without univalence. And I
would agree with this assessment.
Best,
Martin
--
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<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com?utm_medium=email&utm_source=footer>.
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
--
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/F89C9786-6661-4F12-951D-3D58B1D71C6E%40nottingham.ac.uk.
[-- Attachment #2: Type: text/html, Size: 20765 bytes --]
next prev parent reply other threads:[~2019-11-27 10:12 UTC|newest]
Thread overview: 32+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-10-27 14:41 Nicolas Alexander Schmidt
2019-10-27 17:22 ` Bas Spitters
2019-11-03 11:38 ` Bas Spitters
2019-11-03 11:52 ` David Roberts
2019-11-03 19:13 ` Michael Shulman
2019-11-03 19:45 ` Valery Isaev
2019-11-03 22:23 ` Martín Hötzel Escardó
2019-11-04 23:20 ` Nicolas Alexander Schmidt
2019-11-24 18:11 ` Kevin Buzzard
2019-11-26 0:25 ` Michael Shulman
2019-11-26 8:08 ` Ulrik Buchholtz
2019-11-26 19:14 ` Martín Hötzel Escardó
2019-11-26 19:53 ` Kevin Buzzard
2019-11-26 20:40 ` Martín Hötzel Escardó
2019-11-26 22:18 ` Michael Shulman
2019-11-27 0:16 ` Joyal, André
2019-11-27 2:28 ` Stefan Monnier
2019-11-27 1:41 ` Daniel R. Grayson
2019-11-27 8:22 ` N. Raghavendra
2019-11-27 10:12 ` Thorsten Altenkirch [this message]
2019-11-27 16:37 ` Michael Shulman
2019-11-27 20:21 ` Nicolas Alexander Schmidt
2019-11-04 18:42 ` Kevin Buzzard
2019-11-04 21:10 ` Michael Shulman
2019-11-04 23:26 ` David Roberts
2019-11-05 15:43 ` Daniel R. Grayson
2019-11-05 20:29 ` Yuhao Huang
2019-11-06 23:59 ` Daniel R. Grayson
2019-11-05 23:14 ` Martín Hötzel Escardó
2019-11-06 0:06 ` Stefan Monnier
2019-11-11 18:26 ` Licata, Dan
2019-11-03 7:29 ` Michael Shulman
Reply instructions:
You may reply publicly 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=F89C9786-6661-4F12-951D-3D58B1D71C6E@nottingham.ac.uk \
--to=thorsten.altenkirch@nottingham.ac.uk \
--cc=escardo.martin@gmail.com \
--cc=homotopytypetheory@googlegroups.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
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).