Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / Atom feed
* "Identifications" ?
@ 2020-05-04  9:35 Thorsten Altenkirch
  2020-05-04 10:59 ` [HoTT] " stre...
                   ` (2 more replies)
  0 siblings, 3 replies; 26+ messages in thread
From: Thorsten Altenkirch @ 2020-05-04  9:35 UTC (permalink / raw)
  To: homotopyt...@googlegroups.com


[-- Attachment #1: Type: text/plain, Size: 818 bytes --]

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.





[-- Attachment #2: Type: text/html, Size: 2286 bytes --]

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04  9:35 "Identifications" ? Thorsten Altenkirch
@ 2020-05-04 10:59 ` stre...
  2020-05-04 11:04   ` Steve Awodey
  2020-05-04 11:17   ` Thorsten Altenkirch
  2020-05-04 13:16 ` Michael Shulman
  2020-05-07 19:43 ` Martín Hötzel Escardó
  2 siblings, 2 replies; 26+ messages in thread
From: stre... @ 2020-05-04 10:59 UTC (permalink / raw)
  To: Thorsten Altenkirch; +Cc: 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


^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 10:59 ` [HoTT] " stre...
@ 2020-05-04 11:04   ` Steve Awodey
  2020-05-04 11:17   ` Thorsten Altenkirch
  1 sibling, 0 replies; 26+ messages in thread
From: Steve Awodey @ 2020-05-04 11:04 UTC (permalink / raw)
  To: stre...; +Cc: 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:
> 
> 
>> 
>> 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
> 
> -- 
> 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 HomotopyT...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/f23c7b1ada3c6fd99e47a70620c9e278.squirrel%40webmail.mathematik.tu-darmstadt.de.

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 10:59 ` [HoTT] " stre...
  2020-05-04 11:04   ` Steve Awodey
@ 2020-05-04 11:17   ` Thorsten Altenkirch
  2020-05-04 11:42     ` Nicolai Kraus
  2020-05-04 12:06     ` Thomas Streicher
  1 sibling, 2 replies; 26+ messages in thread
From: Thorsten Altenkirch @ 2020-05-04 11:17 UTC (permalink / raw)
  To: stre...@mathematik.tu-darmstadt.de; +Cc: 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





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.





^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 11:17   ` Thorsten Altenkirch
@ 2020-05-04 11:42     ` Nicolai Kraus
  2020-05-04 12:04       ` Thorsten Altenkirch
  2020-05-04 12:06     ` Thomas Streicher
  1 sibling, 1 reply; 26+ messages in thread
From: Nicolai Kraus @ 2020-05-04 11:42 UTC (permalink / raw)
  To: HomotopyTypeTheory

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



^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 11:42     ` Nicolai Kraus
@ 2020-05-04 12:04       ` Thorsten Altenkirch
  0 siblings, 0 replies; 26+ messages in thread
From: Thorsten Altenkirch @ 2020-05-04 12:04 UTC (permalink / raw)
  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


On 04/05/2020, 12:42, "Nicolai Kraus" <nicola...@gmail.com> wrote:

    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


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




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.





^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 11:17   ` Thorsten Altenkirch
  2020-05-04 11:42     ` Nicolai Kraus
@ 2020-05-04 12:06     ` Thomas Streicher
  2020-05-04 12:12       ` Thorsten Altenkirch
  1 sibling, 1 reply; 26+ messages in thread
From: Thomas Streicher @ 2020-05-04 12:06 UTC (permalink / raw)
  To: Thorsten Altenkirch; +Cc: 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

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 12:06     ` Thomas Streicher
@ 2020-05-04 12:12       ` Thorsten Altenkirch
  2020-05-04 12:39         ` Thomas Streicher
  0 siblings, 1 reply; 26+ messages in thread
From: Thorsten Altenkirch @ 2020-05-04 12:12 UTC (permalink / raw)
  To: Thomas Streicher; +Cc: 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

On 04/05/2020, 13:06, "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de> wrote:

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





^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 12:12       ` Thorsten Altenkirch
@ 2020-05-04 12:39         ` Thomas Streicher
  0 siblings, 0 replies; 26+ messages in thread
From: Thomas Streicher @ 2020-05-04 12:39 UTC (permalink / raw)
  To: Thorsten Altenkirch; +Cc: 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).


^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04  9:35 "Identifications" ? Thorsten Altenkirch
  2020-05-04 10:59 ` [HoTT] " stre...
@ 2020-05-04 13:16 ` Michael Shulman
  2020-05-04 14:17   ` Thorsten Altenkirch
  2020-05-04 14:48   ` Stefan Monnier
  2020-05-07 19:43 ` Martín Hötzel Escardó
  2 siblings, 2 replies; 26+ messages in thread
From: Michael Shulman @ 2020-05-04 13:16 UTC (permalink / raw)
  To: Thorsten Altenkirch; +Cc: 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.

On Mon, May 4, 2020 at 2:35 AM Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> 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 HomotopyT...@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.

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 13:16 ` Michael Shulman
@ 2020-05-04 14:17   ` Thorsten Altenkirch
  2020-05-04 14:48   ` Stefan Monnier
  1 sibling, 0 replies; 26+ messages in thread
From: Thorsten Altenkirch @ 2020-05-04 14:17 UTC (permalink / raw)
  To: Michael Shulman; +Cc: 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

On 04/05/2020, 14:17, "Michael Shulman" <shu...@sandiego.edu> wrote:

    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.

    On Mon, May 4, 2020 at 2:35 AM Thorsten Altenkirch
    <Thorsten....@nottingham.ac.uk> 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 HomotopyT...@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.




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.





^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 13:16 ` Michael Shulman
  2020-05-04 14:17   ` Thorsten Altenkirch
@ 2020-05-04 14:48   ` Stefan Monnier
  2020-05-04 15:46     ` Nicolai Kraus
  2020-05-04 15:59     ` Michael Shulman
  1 sibling, 2 replies; 26+ messages in thread
From: Stefan Monnier @ 2020-05-04 14:48 UTC (permalink / raw)
  To: Michael Shulman; +Cc: 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"


^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 14:48   ` Stefan Monnier
@ 2020-05-04 15:46     ` Nicolai Kraus
  2020-05-04 15:57       ` Thorsten Altenkirch
  2020-05-04 15:59     ` Michael Shulman
  1 sibling, 1 reply; 26+ messages in thread
From: Nicolai Kraus @ 2020-05-04 15:46 UTC (permalink / raw)
  To: HomotopyTypeTheory

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

On 04/05/2020 15:48, Stefan Monnier wrote:
>> 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"
>


^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 15:46     ` Nicolai Kraus
@ 2020-05-04 15:57       ` Thorsten Altenkirch
  0 siblings, 0 replies; 26+ messages in thread
From: Thorsten Altenkirch @ 2020-05-04 15:57 UTC (permalink / raw)
  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

On 04/05/2020, 16:47, "homotopyt...@googlegroups.com on behalf of Nicolai Kraus" <homotopyt...@googlegroups.com on behalf of nicola...@gmail.com> wrote:

    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

    On 04/05/2020 15:48, Stefan Monnier wrote:
    >> 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"
    >

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




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.





^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 14:48   ` Stefan Monnier
  2020-05-04 15:46     ` Nicolai Kraus
@ 2020-05-04 15:59     ` Michael Shulman
  2020-05-04 16:07       ` Steve Awodey
  2020-05-04 16:16       ` Joyal, André
  1 sibling, 2 replies; 26+ messages in thread
From: Michael Shulman @ 2020-05-04 15:59 UTC (permalink / raw)
  To: Stefan Monnier; +Cc: 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.

On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote:
>
> > 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"
>

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 15:59     ` Michael Shulman
@ 2020-05-04 16:07       ` Steve Awodey
  2020-05-04 16:17         ` Thorsten Altenkirch
  2020-05-04 16:21         ` Peter LeFanu Lumsdaine
  2020-05-04 16:16       ` Joyal, André
  1 sibling, 2 replies; 26+ messages in thread
From: Steve Awodey @ 2020-05-04 16:07 UTC (permalink / raw)
  To: Michael Shulman
  Cc: 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
> 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.
> 
>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote:
>> 
>>> 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"
>> 
> 
> -- 
> 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 HomotopyT...@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.

^ permalink raw reply	[flat|nested] 26+ messages in thread

* RE: [HoTT] "Identifications" ?
  2020-05-04 15:59     ` Michael Shulman
  2020-05-04 16:07       ` Steve Awodey
@ 2020-05-04 16:16       ` Joyal, André
  2020-05-04 20:38         ` Joyal, André
  1 sibling, 1 reply; 26+ messages in thread
From: Joyal, André @ 2020-05-04 16:16 UTC (permalink / raw)
  To: Michael Shulman, Stefan Monnier
  Cc: 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" ?

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.

On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote:
>
> > 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"
>

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

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 16:07       ` Steve Awodey
@ 2020-05-04 16:17         ` Thorsten Altenkirch
  2020-05-04 16:53           ` Steve Awodey
  2020-05-04 16:21         ` Peter LeFanu Lumsdaine
  1 sibling, 1 reply; 26+ messages in thread
From: Thorsten Altenkirch @ 2020-05-04 16:17 UTC (permalink / raw)
  To: Steve Awodey, Michael Shulman
  Cc: 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

On 04/05/2020, 17:08, "Steve Awodey" <steve...@gmail.com> 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. 
    : - )


    > 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
    > 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.
    > 
    >> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote:
    >> 
    >>> 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"
    >> 
    > 
    > -- 
    > 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 HomotopyT...@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.




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.





^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 16:07       ` Steve Awodey
  2020-05-04 16:17         ` Thorsten Altenkirch
@ 2020-05-04 16:21         ` Peter LeFanu Lumsdaine
  1 sibling, 0 replies; 26+ messages in thread
From: Peter LeFanu Lumsdaine @ 2020-05-04 16:21 UTC (permalink / raw)
  To: Steve Awodey
  Cc: Michael Shulman, Stefan Monnier, Thorsten Altenkirch,
	homotopyt...@googlegroups.com


[-- Attachment #1: Type: text/plain, Size: 3489 bytes --]

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.

On Mon, May 4, 2020 at 6:07 PM Steve Awodey <steve...@gmail.com> 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.
> : - )
>
>
> > 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
> > 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.
> >
> >> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca>
> wrote:
> >>
> >>> 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"
> >>
> >
> > --
> > 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 HomotopyT...@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 HomotopyT...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/E31B538B-E0C9-4D4F-A4F1-4335E59CAE0D%40gmail.com
> .
>

[-- Attachment #2: Type: text/html, Size: 4841 bytes --]

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 16:17         ` Thorsten Altenkirch
@ 2020-05-04 16:53           ` Steve Awodey
  2020-05-04 17:25             ` Thorsten Altenkirch
  0 siblings, 1 reply; 26+ messages in thread
From: Steve Awodey @ 2020-05-04 16:53 UTC (permalink / raw)
  To: Thorsten Altenkirch
  Cc: 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

> 
> Thorsten
> 
> On 04/05/2020, 17:08, "Steve Awodey" <steve...@gmail.com> 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. 
>    : - )
> 
> 
>> 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
>> 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.
>> 
>>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote:
>>> 
>>>> 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"
>>> 
>> 
>> -- 
>> 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 HomotopyT...@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.
> 
> 
> 
> 
> 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 HomotopyT...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D83C2B3E-AF61-409B-BE3A-A98839A00CF6%40nottingham.ac.uk.


^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 16:53           ` Steve Awodey
@ 2020-05-04 17:25             ` Thorsten Altenkirch
  2020-05-04 17:43               ` Michael Shulman
  2020-05-04 17:55               ` Steve Awodey
  0 siblings, 2 replies; 26+ messages in thread
From: Thorsten Altenkirch @ 2020-05-04 17:25 UTC (permalink / raw)
  To: Steve Awodey
  Cc: 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

On 04/05/2020, 17:54, "Steven Awodey on behalf of Steve Awodey" <awo...@andrew.cmu.edu on behalf of awo...@cmu.edu> wrote:



    > 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

    > 
    > Thorsten
    > 
    > On 04/05/2020, 17:08, "Steve Awodey" <steve...@gmail.com> 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. 
    >    : - )
    > 
    > 
    >> 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
    >> 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.
    >> 
    >>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote:
    >>> 
    >>>> 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"
    >>> 
    >> 
    >> -- 
    >> 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 HomotopyT...@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.
    > 
    > 
    > 
    > 
    > 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 HomotopyT...@googlegroups.com.
    > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D83C2B3E-AF61-409B-BE3A-A98839A00CF6%40nottingham.ac.uk.





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.





^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 17:25             ` Thorsten Altenkirch
@ 2020-05-04 17:43               ` Michael Shulman
  2020-05-04 17:55               ` Steve Awodey
  1 sibling, 0 replies; 26+ messages in thread
From: Michael Shulman @ 2020-05-04 17:43 UTC (permalink / raw)
  To: Thorsten Altenkirch
  Cc: 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.

On Mon, May 4, 2020 at 10:25 AM 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.
>
> 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
>
> On 04/05/2020, 17:54, "Steven Awodey on behalf of Steve Awodey" <awo...@andrew.cmu.edu on behalf of awo...@cmu.edu> wrote:
>
>
>
>     > 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
>
>     >
>     > Thorsten
>     >
>     > On 04/05/2020, 17:08, "Steve Awodey" <steve...@gmail.com> 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.
>     >    : - )
>     >
>     >
>     >> 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
>     >> 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.
>     >>
>     >>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote:
>     >>>
>     >>>> 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"
>     >>>
>     >>
>     >> --
>     >> 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 HomotopyT...@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.
>     >
>     >
>     >
>     >
>     > 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 HomotopyT...@googlegroups.com.
>     > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D83C2B3E-AF61-409B-BE3A-A98839A00CF6%40nottingham.ac.uk.
>
>
>
>
>
> 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.
>
>
>
>

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] "Identifications" ?
  2020-05-04 17:25             ` Thorsten Altenkirch
  2020-05-04 17:43               ` Michael Shulman
@ 2020-05-04 17:55               ` Steve Awodey
  1 sibling, 0 replies; 26+ messages in thread
From: Steve Awodey @ 2020-05-04 17:55 UTC (permalink / raw)
  To: Thorsten Altenkirch
  Cc: 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!

Steve

> 
> Thorsten
> 
> On 04/05/2020, 17:54, "Steven Awodey on behalf of Steve Awodey" <awo...@andrew.cmu.edu on behalf of awo...@cmu.edu> wrote:
> 
> 
> 
>> 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
> 
>> 
>> Thorsten
>> 
>> On 04/05/2020, 17:08, "Steve Awodey" <steve...@gmail.com> 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. 
>>   : - )
>> 
>> 
>>> 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
>>> 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.
>>> 
>>>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote:
>>>> 
>>>>> 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"
>>>> 
>>> 
>>> -- 
>>> 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 HomotopyT...@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.
>> 
>> 
>> 
>> 
>> 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 HomotopyT...@googlegroups.com.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D83C2B3E-AF61-409B-BE3A-A98839A00CF6%40nottingham.ac.uk.
> 
> 
> 
> 
> 
> 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.
> 
> 
> 
> 


^ permalink raw reply	[flat|nested] 26+ messages in thread

* RE: [HoTT] "Identifications" ?
  2020-05-04 16:16       ` Joyal, André
@ 2020-05-04 20:38         ` Joyal, André
  0 siblings, 0 replies; 26+ messages in thread
From: Joyal, André @ 2020-05-04 20:38 UTC (permalink / raw)
  To: Michael Shulman, Stefan Monnier
  Cc: 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,

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

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.

On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote:
>
> > 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"
>

--
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 HomotopyT...@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 HomotopyT...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F3F0F%40Pli.gst.uqam.ca.

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: "Identifications" ?
  2020-05-04  9:35 "Identifications" ? Thorsten Altenkirch
  2020-05-04 10:59 ` [HoTT] " stre...
  2020-05-04 13:16 ` Michael Shulman
@ 2020-05-07 19:43 ` Martín Hötzel Escardó
  2020-05-08 10:41   ` [HoTT] " Thorsten Altenkirch
  2 siblings, 1 reply; 26+ messages in thread
From: Martín Hötzel Escardó @ 2020-05-07 19:43 UTC (permalink / raw)
  To: Homotopy Type Theory

[-- Attachment #1.1: Type: text/plain, Size: 1161 bytes --]

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

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

[-- Attachment #1.2: Type: text/html, Size: 1661 bytes --]

^ permalink raw reply	[flat|nested] 26+ messages in thread

* Re: [HoTT] Re: "Identifications" ?
  2020-05-07 19:43 ` Martín Hötzel Escardó
@ 2020-05-08 10:41   ` Thorsten Altenkirch
  0 siblings, 0 replies; 26+ messages in thread
From: Thorsten Altenkirch @ 2020-05-08 10:41 UTC (permalink / raw)
  To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory


[-- Attachment #1: Type: text/plain, Size: 2671 bytes --]



Sent from my iPhone

On 7 May 2020, at 20:43, Martín Hötzel Escardó <escard...@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 HomotopyT...@googlegroups.com<mailto:HomotopyT...@googlegroups.com>.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/994babd9-6067-41a1-b12a-17c149138fdb%40googlegroups.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/994babd9-6067-41a1-b12a-17c149138fdb%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.





[-- Attachment #2: Type: text/html, Size: 3996 bytes --]

^ permalink raw reply	[flat|nested] 26+ messages in thread

end of thread, back to index

Thread overview: 26+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-05-04  9:35 "Identifications" ? Thorsten Altenkirch
2020-05-04 10:59 ` [HoTT] " stre...
2020-05-04 11:04   ` Steve Awodey
2020-05-04 11:17   ` Thorsten Altenkirch
2020-05-04 11:42     ` Nicolai Kraus
2020-05-04 12:04       ` Thorsten Altenkirch
2020-05-04 12:06     ` Thomas Streicher
2020-05-04 12:12       ` Thorsten Altenkirch
2020-05-04 12:39         ` Thomas Streicher
2020-05-04 13:16 ` Michael Shulman
2020-05-04 14:17   ` Thorsten Altenkirch
2020-05-04 14:48   ` Stefan Monnier
2020-05-04 15:46     ` Nicolai Kraus
2020-05-04 15:57       ` Thorsten Altenkirch
2020-05-04 15:59     ` Michael Shulman
2020-05-04 16:07       ` Steve Awodey
2020-05-04 16:17         ` Thorsten Altenkirch
2020-05-04 16:53           ` Steve Awodey
2020-05-04 17:25             ` Thorsten Altenkirch
2020-05-04 17:43               ` Michael Shulman
2020-05-04 17:55               ` Steve Awodey
2020-05-04 16:21         ` Peter LeFanu Lumsdaine
2020-05-04 16:16       ` Joyal, André
2020-05-04 20:38         ` Joyal, André
2020-05-07 19:43 ` Martín Hötzel Escardó
2020-05-08 10:41   ` [HoTT] " Thorsten Altenkirch

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Example config snippet for mirrors

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git