13 views

Skip to first unread message

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.

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
> 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?

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

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.

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.

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

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

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

> 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?
> enlighten me what is the difference between identifications and equality?

> Maybe there is an identification between them but they are not equal? Are

You may identify things which are not equal.

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.

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.

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?
> enlighten me what is the difference between identifications and equality?

> Maybe there is an identification between them but they are not equal? Are

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

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:
> 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?

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

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

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.
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.

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

> 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?

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

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

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

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).

> 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.

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).

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.

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.
> 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.

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

Thorsten

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?
> 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.

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

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

original terminology ("identity type") than "equality" or "path" are.

Nicolai

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

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.
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.

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.

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.

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

: - )

> 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.
> 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.

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.

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.

: - )

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

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/E31B538B-E0C9-4D4F-A4F1-4335E59CAE0D%40gmail.com.

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.
>

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

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

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

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.

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.

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.

>

> 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.

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!

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.

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.

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

May 8, 2020, 6:42:01 AM5/8/20

to Martín Hötzel Escardó, 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.

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/994babd9-6067-41a1-b12a-17c149138fdb%40googlegroups.com.

Reply all

Reply to author

Forward

0 new messages