"Identifications" ?

13 views
Skip to first unread message

Thorsten Altenkirch

unread,
May 4, 2020, 5:35:53 AM5/4/20
to homotopyt...@googlegroups.com

I am just reading a paper which uses the word “Identification” instead of equality. I think this has been proposed by Bob Harper. Can anybody enlighten me what is the difference between identifications and equality? Maybe there is an identification between them but they are not equal? Are the real numbers 0.999… identified or are they equal?

 

Thorsten


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.



stre...@mathematik.tu-darmstadt.de

unread,
May 4, 2020, 6:59:31 AM5/4/20
to Thorsten Altenkirch, homotopyt...@googlegroups.com
> I am just reading a paper which uses the word “Identification” instead
> of equality. I think this has been proposed by Bob Harper. Can anybody
> enlighten me what is the difference between identifications and equality?
> Maybe there is an identification between them but they are not equal? Are
> the real numbers 0.999… identified or are they equal?

You may identify things which are not equal. So ''identify'' seems to mean
consider as equal.
In a sense this is very descriptive for what is going on in HoTT where one
never performs quotients but rather widens equivalence relations.
This is really different in the respective topos models as eg simplicial
sets or already the topos of reflexive graphs as exemplified by N. Kraus's
puzzling counterexample.

Thomas

Steve Awodey

unread,
May 4, 2020, 7:04:13 AM5/4/20
to stre...@mathematik.tu-darmstadt.de, Thorsten Altenkirch, homotopyt...@googlegroups.com
This terminology was first proposed by Dan Grayson in one of our discussions in Simonyi Hall, as a way of understanding the elements of identity types. It’s used occasionally in the book.

Regards,
Steve

> On May 4, 2020, at 06:59, stre...@mathematik.tu-darmstadt.de wrote:
>
> 
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/f23c7b1ada3c6fd99e47a70620c9e278.squirrel%40webmail.mathematik.tu-darmstadt.de.

Thorsten Altenkirch

unread,
May 4, 2020, 7:17:22 AM5/4/20
to stre...@mathematik.tu-darmstadt.de, homotopyt...@googlegroups.com
On 04/05/2020, 12:00, "stre...@mathematik.tu-darmstadt.de" <stre...@mathematik.tu-darmstadt.de> wrote:

> I am just reading a paper which uses the word “Identification†instead
> of equality. I think this has been proposed by Bob Harper. Can anybody
> enlighten me what is the difference between identifications and equality?
> Maybe there is an identification between them but they are not equal? Are
> the real numbers 0.999… identified or are they equal?

You may identify things which are not equal.

Hence my question wether 0.999... and 1 are equal or identified.

My understanding is that 0.999... and 1 as real numbers are equal. That is what we mean by equality in Mathematics. The difference which is introduced here is intensional and doesn't make any sense. We may even ask whether 3+1 and 4 are identified or equal?

So ''identify'' seems to mean
consider as equal.
In a sense this is very descriptive for what is going on in HoTT where one
never performs quotients but rather widens equivalence relations.

I don't understand this. Surely we quotient in HoTT even though the notion of a HIT or even a QIT (i.e. a set level HIT) are more general than ordinary set-quotients.

This is really different in the respective topos models as eg simplicial
sets or already the topos of reflexive graphs as exemplified by N. Kraus's
puzzling counterexample.

What puzzling counterexample is this?

Thorsten

On 04/05/2020, 12:00, "stre...@mathematik.tu-darmstadt.de" <stre...@mathematik.tu-darmstadt.de> wrote:

> I am just reading a paper which uses the word “Identification†instead
> of equality. I think this has been proposed by Bob Harper. Can anybody
> enlighten me what is the difference between identifications and equality?
> Maybe there is an identification between them but they are not equal? Are
> the real numbers 0.999… identified or are they equal?

You may identify things which are not equal. So ''identify'' seems to mean
consider as equal.
In a sense this is very descriptive for what is going on in HoTT where one
never performs quotients but rather widens equivalence relations.
This is really different in the respective topos models as eg simplicial
sets or already the topos of reflexive graphs as exemplified by N. Kraus's
puzzling counterexample.

Thomas

Nicolai Kraus

unread,
May 4, 2020, 7:42:30 AM5/4/20
to HomotopyT...@googlegroups.com
On 04/05/2020 12:17, Thorsten Altenkirch wrote:
> This is really different in the respective topos models as eg simplicial
> sets or already the topos of reflexive graphs as exemplified by N. Kraus's
> puzzling counterexample.
>
> What puzzling counterexample is this?

Thomas was referring to:
https://homotopytypetheory.org/2013/10/28/

You may also have seen it in my thesis or the paper "Notions of
Anonymous Existence in Martin-Löf Type Theory". :)
Nicolai


Thorsten Altenkirch

unread,
May 4, 2020, 8:04:26 AM5/4/20
to nicolai.kraus, homotopyt...@googlegroups.com
I always thought that the "magic trick" would just cause confusion.

It is important to distinguish whether we talk about Mathematics or whether we do Mathematics. The magic trick example works because we confuse the two. Myst reduces to the secret but mathematically there is no inverse. What matters is the latter.

Thorsten
--
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 HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/a2504582-a7f5-6bcb-ebc6-17ae869ebaa8%40gmail.com.

Thomas Streicher

unread,
May 4, 2020, 8:06:24 AM5/4/20
to Thorsten Altenkirch, homotopyt...@googlegroups.com
Hi Thorsten,

> This is really different in the respective topos models as eg simplicial
> sets or already the topos of reflexive graphs as exemplified by N. Kraus's
> puzzling counterexample.
>
> What puzzling counterexample is this?

I learnt it from Nicolai when he gave a little talk at CSL 2017 when
given a prize for his thesis.
The counterexample or rather my appreciation of it I have made a little note
on which I have put for convenience at
https://www.mathematik.tu-darmstadt.de/~streicher/kraus.pdf

The point is that interpreting HoTT in sSet is very different from the
traditional interpretation of logic in sSet. The same happens already
the topos of reflexive graphs. Propositions are connected reflexive
graphs and thee are very man nonisomorphic such guys but HoTT
identifies them all.

But this has nothing to do with HoTT per se. For example you can
interpret HOL in assemblies in two very different ways once `a la
topos (proof irrelevant) and once `a la model of TT (proof relevant).

In mathematics equality is a very relative notion. But one may perform
quotients to reconcile them...

Thomas

Thorsten Altenkirch

unread,
May 4, 2020, 8:12:09 AM5/4/20
to Thomas Streicher, homotopyt...@googlegroups.com
Hi Thomas

But I am not "interpreting HoTT in SSet". I am just working in HoTT. You are doing Metamathematics, I am just talking about Mathematics.

Sure when you consider models of your theory you can say that certain equalities are just metatheoretic equalities and others are non-trivial equalities.

Do you think of a model of set theory when you do set theory?

Cheers,
Thorsten

Thomas Streicher

unread,
May 4, 2020, 8:39:41 AM5/4/20
to Thorsten Altenkirch, homotopyt...@googlegroups.com
Hi Thorsten,

> But I am not "interpreting HoTT in SSet". I am just working in HoTT. You are doing Metamathematics, I am just talking about Mathematics.
>
> Sure when you consider models of your theory you can say that certain equalities are just metatheoretic equalities and others are non-trivial equalities.

I am not sure what you really mean but I guess you refer to the
distinction between what is provable in HoTT and what holds or exists
in particular models. Of couse, Nicolai"s vexing example is model
dependent (at least in my reconstruction!)
But that is the same in set theory. Most of the time you are model
independent, i.e. provable in ZFC or actually much weaker systems. But
there are quite a few things which heavily depend on the
model. Continuum Hypothesis for example but many other things as well.
Modern set theory is essentially about independences...

And if you consider ZF the notions of finite and Dedekind finite are
different. That is in my opinion an example where incompleteness
strikes already on a very basic level!

Thomas

PS But I agree that this is "metamathematical" but so what.
Mathematics is not one fixed game but rather pluralist even classically.
Even more so constructively where things branch much earlier. As a
(categorical) logician one is interested in constructive mathematics
precisely because of this excessive pluralism!
I never understood why constructive math is used in the singular since
it is even false for classical maths.

And adding strong principles doesn't mean one gets nonalgorithmic.
Adding to HA all true Pi^0_1 sentences doesn't allow you to construct
functions on N which are not recursive (as follow from number realizability).

Michael Shulman

unread,
May 4, 2020, 9:17:13 AM5/4/20
to Thorsten Altenkirch, homotopyt...@googlegroups.com
I don't think using "identification" necessarily implies any
difference between "identification" and "equality". I don't think of
it that way. For me the point is just to have a word that refers to
an *element* of an identity type. Calling it "an equality" can have
the wrong connotation because classically, an equality is just a
proposition (or a true proposition), whereas an element of an identity
type carries information. Calling it "an identification" suggests
exactly the information that it carries: a way of identifying two
things.
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/BBC0B8F3-AB16-4196-B9B9-B1B3031B2D7D%40nottingham.ac.uk.

Thorsten Altenkirch

unread,
May 4, 2020, 10:17:31 AM5/4/20
to Michael Shulman, homotopyt...@googlegroups.com
This seems reasonable. I usually say "equality proofs" but the word proof also has other conotations. Also what is an element of 3 <= 4, if not a proof or evidence? Maybe it is a inidentification? __

Thorsten

Stefan Monnier

unread,
May 4, 2020, 10:48:34 AM5/4/20
to Michael Shulman, Thorsten Altenkirch, homotopyt...@googlegroups.com
> I don't think using "identification" necessarily implies any
> difference between "identification" and "equality". I don't think of
> it that way. For me the point is just to have a word that refers to
> an *element* of an identity type. Calling it "an equality" can have
> the wrong connotation because classically, an equality is just a
> proposition (or a true proposition), whereas an element of an identity
> type carries information. Calling it "an identification" suggests
> exactly the information that it carries: a way of identifying two
> things.

I thought that's what "path" was for?


Stefan "who really doesn't know what he's talking about"

Nicolai Kraus

unread,
May 4, 2020, 11:46:46 AM5/4/20
to HomotopyT...@googlegroups.com
For what it's worth, "identification" is much closer to Per Martin-Löf's
original terminology ("identity type") than "equality" or "path" are.
Nicolai

Thorsten Altenkirch

unread,
May 4, 2020, 11:57:57 AM5/4/20
to nicolai.kraus, homotopyt...@googlegroups.com
Ok, I apologize discussions on names and syntax are at the same time very attractive and are also scoffed at because they seem not to have much content.

I am quite happy with Mike's explanation to use the word "identifications" for inhabitants of equality types. "Paths" or "equality proofs" or "evidence for equality" are also good alternatives.

However, I prefer to use the word "equality" even equality is not propositional. Two mathematical objects which share all properties we can talk about should be considered equal even if there is more than one reason / proof / identification that this is the case. Moreover, there is no other "equality" we can talk about in Type Theory.

Thorsten
--
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 HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/b1b554b1-1c70-0bd6-5c09-cd5f0f2e48f9%40gmail.com.

Michael Shulman

unread,
May 4, 2020, 12:00:06 PM5/4/20
to Stefan Monnier, Thorsten Altenkirch, homotopyt...@googlegroups.com
The word "path" is closely tied to the homotopy interpretation, and to
the classical perspective of oo-groupoids presented via topological
spaces, which has various problems. This is particularly an issue in
cohesive type theory, where there is a separate "point-set level"
notion of path that it is important to distinguish from
identifications.

Steve Awodey

unread,
May 4, 2020, 12:07:53 PM5/4/20
to Michael Shulman, Stefan Monnier, Thorsten Altenkirch, homotopyt...@googlegroups.com
I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago.
: - )


> On May 4, 2020, at 12:00, Michael Shulman <shu...@sandiego.edu> wrote:
>
> The word "path" is closely tied to the homotopy interpretation, and to
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%40mail.gmail.com.

Joyal, André

unread,
May 4, 2020, 12:16:30 PM5/4/20
to Michael Shulman, Stefan Monnier, Thorsten Altenkirch, homotopyt...@googlegroups.com
Dear all,

I am tempted to add my grain of salt to this discussion.
I like the word "identification".
But what about "iso" ?
It means "equal". As in "iso-morphism", "iso-tope", etc.

https://wordinfo.info/unit/2795/page:9

Best,
André

________________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Michael Shulman [shu...@sandiego.edu]
Sent: Monday, May 04, 2020 11:59 AM
To: Stefan Monnier
Cc: Thorsten Altenkirch; homotopyt...@googlegroups.com
Subject: Re: [HoTT] "Identifications" ?

--


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 HomotopyTypeThe...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%40mail.gmail.com.

Thorsten Altenkirch

unread,
May 4, 2020, 12:17:06 PM5/4/20
to Steve Awodey, Michael Shulman, Stefan Monnier, homotopyt...@googlegroups.com

I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago.
: - )

One of our dogs gained access to my laptop - sorry. These animals can be very awkward.

However, even the real Thorsten had a friendly argument with Andre Joyal when we were writing the book about whether to use = for the equality type.

Thorsten

Peter LeFanu Lumsdaine

unread,
May 4, 2020, 12:21:35 PM5/4/20
to Steve Awodey, Michael Shulman, Stefan Monnier, Thorsten Altenkirch, homotopyt...@googlegroups.com
Ah, I just thought the whole system was having a clock malfunction and re-sending a discussion from 2016…  :-P

On the serious side: one motivation for “identification” not yet mentioned is that it’s more in line with traditional mathematical usage.  Saying that the circle defined as R/Z or as a subset of R^2 are “equal” clashes badly with the traditional mathematical usage of words, and (for at least some mathematicians) their mental picture of mathematics — but saying that we can identify them, and that all nice properties respect such identifications, is completely consistent with traditional writing and worldviews.  Also, the fact that we may identify things in multiple ways, and so have to be a little careful about how we make use of such identifications, fits with traditional intuition and practice.

So saying “identifications” may require less rewiring in our brains than saying “equalities” or “paths”, at least in types of algebraic structures and similar.  (For synthetic homotopy theory, of course, “paths” often fits closer to established usage.)

–p.

Steve Awodey

unread,
May 4, 2020, 12:54:04 PM5/4/20
to Thorsten Altenkirch, Michael Shulman, Stefan Monnier, homotopyt...@googlegroups.com


> On May 4, 2020, at 12:17 PM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote:
>
>
> I’m afraid that someone may have hacked Thorsten’s email account. The real Thorsten went through all this with us many years ago.
> : - )
>
> One of our dogs gained access to my laptop - sorry. These animals can be very awkward.
>
> However, even the real Thorsten had a friendly argument with Andre Joyal when we were writing the book about whether to use = for the equality type.

I remember that conversation.
I think we decided to put the question “what does x=y mean?” aside,
until we had taken care of more important things.

So is it time now?

Steve
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D83C2B3E-AF61-409B-BE3A-A98839A00CF6%40nottingham.ac.uk.

Thorsten Altenkirch

unread,
May 4, 2020, 1:25:07 PM5/4/20
to Steve Awodey, Michael Shulman, Stefan Monnier, homotopyt...@googlegroups.com
Hi Steve,

I remember that conversation.
I think we decided to put the question “what does x=y mean?” aside,
until we had taken care of more important things.

I suppose this was just a way to move on without having to reach an agreement.

I think it is more than a discussion about terms. What do we mean by equality? Does the equality type in HoTT is something fundamentally different? In a way yes, because it is proof relevant so some of the old terminology doesn't apply anymore. That is equality of structures is a structure not a proposition. But nevertheless I find it confusing to call it anything but equality. I would say two mathematical objects which share all the same properties, which behave the same, are equal. I don't like Leibniz's "equality of indiscernibles" because it uses a negative.

I noticed that many people use type theory always as something we talk about. It is just a formalism. Hence the equality type just expresses an identification of things which are actually different. In the real world. However, I think when we talk in type theory then this is our real world (at least metaphorically) and then the metatheoretic perspective is just a confusion.

Does this make sense? Sorry, I realize it is a bit philosophical but then you are in the department of philosophy... __

Thorsten

Michael Shulman

unread,
May 4, 2020, 1:43:18 PM5/4/20
to Thorsten Altenkirch, Steve Awodey, Stefan Monnier, homotopyt...@googlegroups.com
I think "identification" is a nice middle-ground between "equality"
and "path/isomorphism". On the one hand it signals that something
more is meant than the thing traditionally called "equality" (even
though I agree with Thorsten that inside of type theory this is the
thing called "equality") -- and, I think, does a good job of
suggesting precisely *what* more is meant. On the other hand, it
still carries the meaning that two things are *the same* (in a
particular way) -- two things that have been "identified" are now
"identical" -- whereas "path" and "isomorphism" suggest their
traditional meanings of two things that are *not* fundamentally the
same but are related in some same-like-way.

Steve Awodey

unread,
May 4, 2020, 1:55:19 PM5/4/20
to Thorsten Altenkirch, Michael Shulman, Stefan Monnier, homotopyt...@googlegroups.com


> On May 4, 2020, at 1:25 PM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote:
>
> Hi Steve,
>
> I remember that conversation.
> I think we decided to put the question “what does x=y mean?” aside,
> until we had taken care of more important things.
>
> I suppose this was just a way to move on without having to reach an agreement.

yup

>
> I think it is more than a discussion about terms. What do we mean by equality? Does the equality type in HoTT is something fundamentally different? In a way yes, because it is proof relevant so some of the old terminology doesn't apply anymore. That is equality of structures is a structure not a proposition. But nevertheless I find it confusing to call it anything but equality. I would say two mathematical objects which share all the same properties, which behave the same, are equal. I don't like Leibniz's "equality of indiscernibles" because it uses a negative.

you seem to prefer the term “equality” over “identity” - even when (mis)quoting Leibniz!

maybe that’s part of the problem: if we talk about “identity types” instead of “equality types” then it’s easier to regard them as structures,
the inhabitants of which are “identifications”, rather than “equality proofs” (which introduces an unwanted meta-perspective).

Frege once considered equality as a relation between symbols, rather than what they denote — he later rejected that view, but I don’t think it's so bad.
Definitional equality can be thought of like this — it’s a meta-statement about (pseudo-) syntactic things.
The relation that we can reason about inside the system is called *identity*, and it’s a "proof relevant” relation
— or better put, it’s a proper structure, not a mere proposition —
its elements are identifications, and these we know admit an oo-groupoid structure.

>
> Does this make sense? Sorry, I realize it is a bit philosophical but then you are in the department of philosophy… __

to my everlasting regret — and thanks for not calling me a philosopher!

Joyal, André

unread,
May 4, 2020, 4:38:54 PM5/4/20
to Michael Shulman, Stefan Monnier, Thorsten Altenkirch, homotopyt...@googlegroups.com
Of course, the term "identification" has other meanings.
As when the police is trying to identify the victim of a murder.
An identification may require an identity document.
A hacker may prefer to stay anonymous.

The term "iso" could be better.
Let f:a=b be an iso between the elements a and b of a type A.
Let f:A=B be an isomorphism between the types A and B.
The univalence principle state that every isomorphism is an iso.

A
________________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Joyal, André [joyal...@uqam.ca]
Sent: Monday, May 04, 2020 12:16 PM
To: Michael Shulman; Stefan Monnier
Cc: Thorsten Altenkirch; homotopyt...@googlegroups.com
Subject: RE: [HoTT] "Identifications" ?

Dear all,

https://wordinfo.info/unit/2795/page:9

Best,
André

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F3F0F%40Pli.gst.uqam.ca.

Martín Hötzel Escardó

unread,
May 7, 2020, 3:43:27 PM5/7/20
to Homotopy Type Theory
The meanings of "equal" and "identical" are the same. They both mean "same", and are equivalent to "equivalent" according to most dictionaries. 

Try not to be too judgmental, Thorsten.

Best,
Martin

Thorsten Altenkirch

unread,
May 8, 2020, 6:42:01 AM5/8/20
to Martín Hötzel Escardó, Homotopy Type Theory


Sent from my iPhone

On 7 May 2020, at 20:43, Martín Hötzel Escardó <escardo...@gmail.com> wrote:


The meanings of "equal" and "identical" are the same. They both mean "same", and are equivalent to "equivalent" according to most dictionaries. 

I know. My point was rather that there is no need to replace equality/identity by another word, eg identification to suggest that equality in HoTT is anything fundamentally different. My impression is that some people think that equality in HoTT is something different to true equality as it occurs in nature.


Try not to be too judgmental, Thorsten.

What do you mean?

Maybe you shouldn’t jump to conclusions what you think I mean too quickly, Martin.

Thorsten



Best,
Martin

On Monday, 4 May 2020 10:35:53 UTC+1, Thorsten Altenkirch wrote:

I am just reading a paper which uses the word “Identification” instead of equality. I think this has been proposed by Bob Harper. Can anybody enlighten me what is the difference between identifications and equality? Maybe there is an identification between them but they are not equal? Are the real numbers 0.999… identified or are they equal?

 

Thorsten

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 HomotopyTypeThe...@googlegroups.com.
Reply all
Reply to author
Forward
0 new messages