Discussion of Homotopy Type Theory and Univalent Foundations
help / color / mirror / Atom feed
* Identity versus equality
@ 2020-05-05  8:47 Ansten Mørch Klev
2020-05-06 16:02  [HoTT] " Joyal, André
From: Ansten Mørch Klev @ 2020-05-05  8:47 UTC (permalink / raw)
To: HomotopyTypeTheory

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

The discussion yesterday provides a good occasion for me to pose a question
I have long wanted to put to this list: is there a convention generally
agreed upon in the HoTT-community for when (if ever) to use 'identity'

Here are some relevant data.

A Germanic equivalent for 'identity' is 'sameness'.
A Germanic equivalent for 'equality' is 'likeness'.

For Aristotle equality means sameness of quantity. This is how one must
understand 'equal' in Euclid's Elements, where a triangle may have all
sides equal (clearly, they cannot be identical). The axiom in the Elements
that has given rise to the term 'Euclidean relation' and which is appealed
to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'.

In Diophantus's Arithmetica, on the other hand, the two terms of an
equation are said to be equal, not identical, and this would become the
standard terminology in algebra. For instance, the sign '=' was introduced
by Robert Recorde as a sign of equality, not as a sign of identity. The
explanation for this apparent discrepancy with the Aristotelian/Euclidean
terminology might be that when dealing with numbers, equality just is
identity, since for two numbers to be identical as to magnitude just is for
them to be the same number. Aristotle says as much in Metaphysics M.7.

Hilbert and Bernays might be one of the few logic books in the modern era
to distinguish equality from identity (volume I, chapter 5). 'Equality' is
there used for any equivalence relation and glossed as the obtaining of
"irgendeine Art von Übereinstimmung". Identity, by contrast, is
"Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility
within the given language.

Frege, by contrast, explicitly identifies (sic!) equality with identity,
and glosses the latter as sameness or coincidence, in the first footnote to
his paper on sense and reference.  Kleene and Church do the same in their
famous textbooks: if one looks under 'identity' in the index to any of
those books one is referred to 'equality'.

Clearly the two cannot be assumed to mean the same by analysts who speak of
two functions being identically equal!

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

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

* RE: [HoTT] Identity versus equality
2020-05-05  8:47 Identity versus equality Ansten Mørch Klev
@ 2020-05-06 16:02  Joyal, André
2020-05-06 19:01    Steve Awodey
From: Joyal, André @ 2020-05-06 16:02 UTC (permalink / raw)

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

Dear all,

A few more thoughts.
We all agree that terminology and notation are important.

I love the story of the equality sign = introduced by Robert Recorde (1512-1558).
"because no two things can be more equal than a pair of parallel lines".
It took more than a century before been universally adopted.
René Descartes (1596-1650) used a different symbol  in his work (something like \alpha).
We may ask why Recorde's notation won over Descartes's notation?
Of course, we may never know.
I dare to say that Recorde's notation was *better*.
Among other things, the equality sign = is symmetric:
the expression a=b and b=a are mirror image of each other.
Recorde's motive for introducing the notation was more about
convenience and aesthetic than about philosophy and history.
It was not because Recorde was a powerful academic,
since he eventually died in prison.

There is something to learn from the history of the equality sign.
I guess that it can also applied to terminology.
A new notation or terminology has a good chance to be adopted universally
if it is simple and useful, but it may take time.

André
________________________________
Sent: Tuesday, May 05, 2020 4:47 AM
Subject: [HoTT] Identity versus equality

The discussion yesterday provides a good occasion for me to pose a question I have long wanted to put to this list: is there a convention generally agreed upon in the HoTT-community for when (if ever) to use 'identity' instead of 'equality'?

Here are some relevant data.

A Germanic equivalent for 'identity' is 'sameness'.
A Germanic equivalent for 'equality' is 'likeness'.

For Aristotle equality means sameness of quantity. This is how one must understand 'equal' in Euclid's Elements, where a triangle may have all sides equal (clearly, they cannot be identical). The axiom in the Elements that has given rise to the term 'Euclidean relation' and which is appealed to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'.

In Diophantus's Arithmetica, on the other hand, the two terms of an equation are said to be equal, not identical, and this would become the standard terminology in algebra. For instance, the sign '=' was introduced by Robert Recorde as a sign of equality, not as a sign of identity. The explanation for this apparent discrepancy with the Aristotelian/Euclidean terminology might be that when dealing with numbers, equality just is identity, since for two numbers to be identical as to magnitude just is for them to be the same number. Aristotle says as much in Metaphysics M.7.

Hilbert and Bernays might be one of the few logic books in the modern era to distinguish equality from identity (volume I, chapter 5). 'Equality' is there used for any equivalence relation and glossed as the obtaining of "irgendeine Art von Übereinstimmung". Identity, by contrast, is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility within the given language.

Frege, by contrast, explicitly identifies (sic!) equality with identity, and glosses the latter as sameness or coincidence, in the first footnote to his paper on sense and reference.  Kleene and Church do the same in their famous textbooks: if one looks under 'identity' in the index to any of those books one is referred to 'equality'.

Clearly the two cannot be assumed to mean the same by analysts who speak of two functions being identically equal!

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

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

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

* Re: [HoTT] Identity versus equality
2020-05-06 16:02  [HoTT] " Joyal, André
@ 2020-05-06 19:01    Steve Awodey
2020-05-06 19:18      Michael Shulman
From: Steve Awodey @ 2020-05-06 19:01 UTC (permalink / raw)

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

Dear Andre’ (and all),

The sign a = b is pretty well established in mathematics as meaning “a equals b”,
which does indeed clash with our choice in the book to use it for the identity type,
and to call the elements of this type “identifications”.
Thorsten has rightly pointed out this clash.

Although I am personally not eager to make any changes in our current terminology and/or notation,
I’m certainly glad to consider the possibiiy
(we did agree to return to this question at some point, so maybe this is it : - ).

We need both symbols and words for two notions:

- judgemental equality, currently a\equiv b,
- propositional equality, currently a = b, short for Id(a,b).

There seems to be a proposal to revise this to something like:

- judgemental equality: written a = b and pronounced “a equals b”,
- propositional equality, written maybe a \cong b, and pronunced ”a iso b”,
(the elements of this type are called “isos").

Another (partial) option would be:

- judgemental equality: written a = b and pronounced “a equals b”,
- propositional equality, written Id(a,b) and shortened somehow a ? b,
and pronunced ”a idenitfied with b”
(the elements of this type are called “identifications").

Do either of these seem preferable?
Are there other proposals?
And how should one decide?

Regards,

Steve

> On May 6, 2020, at 12:02 PM, Joyal, André <joyal...@uqam.ca> wrote:
>
> Dear all,
>
> A few more thoughts.
> We all agree that terminology and notation are important.
>
> I love the story of the equality sign = introduced by Robert Recorde (1512-1558).
> "because no two things can be more equal than a pair of parallel lines".
> It took more than a century before been universally adopted.
> René Descartes (1596-1650) used a different symbol  in his work (something like \alpha).
> We may ask why Recorde's notation won over Descartes's notation?
> Of course, we may never know.
> I dare to say that Recorde's notation was *better*.
> Among other things, the equality sign = is symmetric:
> the expression a=b and b=a are mirror image of each other.
> Recorde's motive for introducing the notation was more about
> convenience and aesthetic than about philosophy and history.
> The notation was gradually adopted because it is simple and useful.
> It was not because Recorde was a powerful academic,
> since he eventually died in prison.
>
> There is something to learn from the history of the equality sign.
> I guess that it can also applied to terminology.
> A new notation or terminology has a good chance to be adopted universally
> if it is simple and useful, but it may take time.
>
> André
> Sent: Tuesday, May 05, 2020 4:47 AM
> Subject: [HoTT] Identity versus equality
>
> The discussion yesterday provides a good occasion for me to pose a question I have long wanted to put to this list: is there a convention generally agreed upon in the HoTT-community for when (if ever) to use 'identity' instead of 'equality'?
>
> Here are some relevant data.
>
> A Germanic equivalent for 'identity' is 'sameness'.
> A Germanic equivalent for 'equality' is 'likeness'.
>
> For Aristotle equality means sameness of quantity. This is how one must understand 'equal' in Euclid's Elements, where a triangle may have all sides equal (clearly, they cannot be identical). The axiom in the Elements that has given rise to the term 'Euclidean relation' and which is appealed to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'.
>
> In Diophantus's Arithmetica, on the other hand, the two terms of an equation are said to be equal, not identical, and this would become the standard terminology in algebra. For instance, the sign '=' was introduced by Robert Recorde as a sign of equality, not as a sign of identity. The explanation for this apparent discrepancy with the Aristotelian/Euclidean terminology might be that when dealing with numbers, equality just is identity, since for two numbers to be identical as to magnitude just is for them to be the same number. Aristotle says as much in Metaphysics M.7.
>
> Hilbert and Bernays might be one of the few logic books in the modern era to distinguish equality from identity (volume I, chapter 5). 'Equality' is there used for any equivalence relation and glossed as the obtaining of "irgendeine Art von Übereinstimmung". Identity, by contrast, is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility within the given language.
>
> Frege, by contrast, explicitly identifies (sic!) equality with identity, and glosses the latter as sameness or coincidence, in the first footnote to his paper on sense and reference.  Kleene and Church do the same in their famous textbooks: if one looks under 'identity' in the index to any of those books one is referred to 'equality'.
>
> Clearly the two cannot be assumed to mean the same by analysts who speak of two functions being identically equal!
>
> --
> 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>.
>
> --
> 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>.

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

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

* Re: [HoTT] Identity versus equality
2020-05-06 19:01    Steve Awodey
@ 2020-05-06 19:18      Michael Shulman
2020-05-06 19:31        Steve Awodey
2020-05-06 22:54        Thorsten Altenkirch
0 siblings, 2 replies; 61+ messages in thread
From: Michael Shulman @ 2020-05-06 19:18 UTC (permalink / raw)
To: Steve Awodey; +Cc: Joyal, André, HomotopyT...@googlegroups.com

As I've said before, I strongly disagree that the standard
interpretation of "a=b" as meaning "a equals b" clashes in any way
with its use to denote the identity type.  Almost without exception,
whenever a mathematican working informally says "equals", that *must*
be formalized as referring to the identity type.  Ask any
mathematician on the street whether x+y=y+x for all natural numbers x
and y, and they will say yes.  But this is false if = means judgmental
equality.  Judgmental equality is a technical object of type theory
that the "generic mathematician" is not aware of at all, so it cannot
co-opt the standard notation "=" or word "equals" if we want "informal
type theory" to be at all comprehensible to such readers.

On Wed, May 6, 2020 at 12:01 PM Steve Awodey <awo...@cmu.edu> wrote:
>
> Dear Andre’ (and all),
>
> The sign a = b is pretty well established in mathematics as meaning “a equals b”,
> which does indeed clash with our choice in the book to use it for the identity type,
> and to call the elements of this type “identifications”.
> Thorsten has rightly pointed out this clash.
>
> Although I am personally not eager to make any changes in our current terminology and/or notation,
> I’m certainly glad to consider the possibiiy
> (we did agree to return to this question at some point, so maybe this is it : - ).
>
> We need both symbols and words for two notions:
>
> - judgemental equality, currently a\equiv b,
> - propositional equality, currently a = b, short for Id(a,b).
>
> There seems to be a proposal to revise this to something like:
>
> - judgemental equality: written a = b and pronounced “a equals b”,
> - propositional equality, written maybe a \cong b, and pronunced ”a iso b”,
> (the elements of this type are called “isos").
>
> Another (partial) option would be:
>
> - judgemental equality: written a = b and pronounced “a equals b”,
> - propositional equality, written Id(a,b) and shortened somehow a ? b,
> and pronunced ”a idenitfied with b”
> (the elements of this type are called “identifications").
>
> Do either of these seem preferable?
> Are there other proposals?
> And how should one decide?
>
> Regards,
>
> Steve
>
>
>
>
>
> On May 6, 2020, at 12:02 PM, Joyal, André <joyal...@uqam.ca> wrote:
>
> Dear all,
>
> A few more thoughts.
> We all agree that terminology and notation are important.
>
> I love the story of the equality sign = introduced by Robert Recorde (1512-1558).
> "because no two things can be more equal than a pair of parallel lines".
> It took more than a century before been universally adopted.
> René Descartes (1596-1650) used a different symbol  in his work (something like \alpha).
> We may ask why Recorde's notation won over Descartes's notation?
> Of course, we may never know.
> I dare to say that Recorde's notation was *better*.
> Among other things, the equality sign = is symmetric:
> the expression a=b and b=a are mirror image of each other.
> Recorde's motive for introducing the notation was more about
> convenience and aesthetic than about philosophy and history.
> The notation was gradually adopted because it is simple and useful.
> It was not because Recorde was a powerful academic,
> since he eventually died in prison.
>
> There is something to learn from the history of the equality sign.
> I guess that it can also applied to terminology.
> A new notation or terminology has a good chance to be adopted universally
> if it is simple and useful, but it may take time.
>
> André
> ________________________________
> Sent: Tuesday, May 05, 2020 4:47 AM
> Subject: [HoTT] Identity versus equality
>
> The discussion yesterday provides a good occasion for me to pose a question I have long wanted to put to this list: is there a convention generally agreed upon in the HoTT-community for when (if ever) to use 'identity' instead of 'equality'?
>
> Here are some relevant data.
>
> A Germanic equivalent for 'identity' is 'sameness'.
> A Germanic equivalent for 'equality' is 'likeness'.
>
> For Aristotle equality means sameness of quantity. This is how one must understand 'equal' in Euclid's Elements, where a triangle may have all sides equal (clearly, they cannot be identical). The axiom in the Elements that has given rise to the term 'Euclidean relation' and which is appealed to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'.
>
> In Diophantus's Arithmetica, on the other hand, the two terms of an equation are said to be equal, not identical, and this would become the standard terminology in algebra. For instance, the sign '=' was introduced by Robert Recorde as a sign of equality, not as a sign of identity. The explanation for this apparent discrepancy with the Aristotelian/Euclidean terminology might be that when dealing with numbers, equality just is identity, since for two numbers to be identical as to magnitude just is for them to be the same number. Aristotle says as much in Metaphysics M.7.
>
> Hilbert and Bernays might be one of the few logic books in the modern era to distinguish equality from identity (volume I, chapter 5). 'Equality' is there used for any equivalence relation and glossed as the obtaining of "irgendeine Art von Übereinstimmung". Identity, by contrast, is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility within the given language.
>
> Frege, by contrast, explicitly identifies (sic!) equality with identity, and glosses the latter as sameness or coincidence, in the first footnote to his paper on sense and reference.  Kleene and Church do the same in their famous textbooks: if one looks under 'identity' in the index to any of those books one is referred to 'equality'.
>
> Clearly the two cannot be assumed to mean the same by analysts who speak of two functions being identically equal!
>
> --
> 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/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%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/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca.
>
>
> --
> 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/05375057-883F-4487-8919-2579F5771AFC%40cmu.edu.

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

* Re: [HoTT] Identity versus equality
2020-05-06 19:18      Michael Shulman
@ 2020-05-06 19:31        Steve Awodey
2020-05-06 20:30          Joyal, André
2020-05-06 22:52          Thorsten Altenkirch
2020-05-06 22:54        Thorsten Altenkirch
1 sibling, 2 replies; 61+ messages in thread
From: Steve Awodey @ 2020-05-06 19:31 UTC (permalink / raw)
To: Michael Shulman

I totally agree with you, Mike.

But I think Thorsten was pointing out (he will correct me if I’m wrong)
that a = b meaning “equals” is maybe not the same as “identity”?

and I do think that the terminology “identification” is good for the elements of this type, which traditionally was called the “identity type".

maybe the answer is to say that mathematics simply doesn’t deal with the “metaphysical" notion of “identity”, as distinct from equality.
we just use both words interchangeably for the single notion expressd by a = b, which is short for Id(a,b).

> On May 6, 2020, at 3:18 PM, Michael Shulman <shu...@sandiego.edu> wrote:
>
> As I've said before, I strongly disagree that the standard
> interpretation of "a=b" as meaning "a equals b" clashes in any way
> with its use to denote the identity type.  Almost without exception,
> whenever a mathematican working informally says "equals", that *must*
> be formalized as referring to the identity type.  Ask any
> mathematician on the street whether x+y=y+x for all natural numbers x
> and y, and they will say yes.  But this is false if = means judgmental
> equality.  Judgmental equality is a technical object of type theory
> that the "generic mathematician" is not aware of at all, so it cannot
> co-opt the standard notation "=" or word "equals" if we want "informal
> type theory" to be at all comprehensible to such readers.
>
>
> On Wed, May 6, 2020 at 12:01 PM Steve Awodey <awo...@cmu.edu> wrote:
>>
>> Dear Andre’ (and all),
>>
>> The sign a = b is pretty well established in mathematics as meaning “a equals b”,
>> which does indeed clash with our choice in the book to use it for the identity type,
>> and to call the elements of this type “identifications”.
>> Thorsten has rightly pointed out this clash.
>>
>> Although I am personally not eager to make any changes in our current terminology and/or notation,
>> I’m certainly glad to consider the possibiiy
>> (we did agree to return to this question at some point, so maybe this is it : - ).
>>
>> We need both symbols and words for two notions:
>>
>> - judgemental equality, currently a\equiv b,
>> - propositional equality, currently a = b, short for Id(a,b).
>>
>> There seems to be a proposal to revise this to something like:
>>
>> - judgemental equality: written a = b and pronounced “a equals b”,
>> - propositional equality, written maybe a \cong b, and pronunced ”a iso b”,
>> (the elements of this type are called “isos").
>>
>> Another (partial) option would be:
>>
>> - judgemental equality: written a = b and pronounced “a equals b”,
>> - propositional equality, written Id(a,b) and shortened somehow a ? b,
>> and pronunced ”a idenitfied with b”
>> (the elements of this type are called “identifications").
>>
>> Do either of these seem preferable?
>> Are there other proposals?
>> And how should one decide?
>>
>> Regards,
>>
>> Steve
>>
>>
>>
>>
>>
>> On May 6, 2020, at 12:02 PM, Joyal, André <joyal...@uqam.ca> wrote:
>>
>> Dear all,
>>
>> A few more thoughts.
>> We all agree that terminology and notation are important.
>>
>> I love the story of the equality sign = introduced by Robert Recorde (1512-1558).
>> "because no two things can be more equal than a pair of parallel lines".
>> It took more than a century before been universally adopted.
>> René Descartes (1596-1650) used a different symbol  in his work (something like \alpha).
>> We may ask why Recorde's notation won over Descartes's notation?
>> Of course, we may never know.
>> I dare to say that Recorde's notation was *better*.
>> Among other things, the equality sign = is symmetric:
>> the expression a=b and b=a are mirror image of each other.
>> Recorde's motive for introducing the notation was more about
>> convenience and aesthetic than about philosophy and history.
>> The notation was gradually adopted because it is simple and useful.
>> It was not because Recorde was a powerful academic,
>> since he eventually died in prison.
>>
>> There is something to learn from the history of the equality sign.
>> I guess that it can also applied to terminology.
>> A new notation or terminology has a good chance to be adopted universally
>> if it is simple and useful, but it may take time.
>>
>> André
>> ________________________________
>> Sent: Tuesday, May 05, 2020 4:47 AM
>> Subject: [HoTT] Identity versus equality
>>
>> The discussion yesterday provides a good occasion for me to pose a question I have long wanted to put to this list: is there a convention generally agreed upon in the HoTT-community for when (if ever) to use 'identity' instead of 'equality'?
>>
>> Here are some relevant data.
>>
>> A Germanic equivalent for 'identity' is 'sameness'.
>> A Germanic equivalent for 'equality' is 'likeness'.
>>
>> For Aristotle equality means sameness of quantity. This is how one must understand 'equal' in Euclid's Elements, where a triangle may have all sides equal (clearly, they cannot be identical). The axiom in the Elements that has given rise to the term 'Euclidean relation' and which is appealed to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'.
>>
>> In Diophantus's Arithmetica, on the other hand, the two terms of an equation are said to be equal, not identical, and this would become the standard terminology in algebra. For instance, the sign '=' was introduced by Robert Recorde as a sign of equality, not as a sign of identity. The explanation for this apparent discrepancy with the Aristotelian/Euclidean terminology might be that when dealing with numbers, equality just is identity, since for two numbers to be identical as to magnitude just is for them to be the same number. Aristotle says as much in Metaphysics M.7.
>>
>> Hilbert and Bernays might be one of the few logic books in the modern era to distinguish equality from identity (volume I, chapter 5). 'Equality' is there used for any equivalence relation and glossed as the obtaining of "irgendeine Art von Übereinstimmung". Identity, by contrast, is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility within the given language.
>>
>> Frege, by contrast, explicitly identifies (sic!) equality with identity, and glosses the latter as sameness or coincidence, in the first footnote to his paper on sense and reference.  Kleene and Church do the same in their famous textbooks: if one looks under 'identity' in the index to any of those books one is referred to 'equality'.
>>
>> Clearly the two cannot be assumed to mean the same by analysts who speak of two functions being identically equal!
>>
>> --
>> 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/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%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/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca.
>>
>>
>> --
>> 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/05375057-883F-4487-8919-2579F5771AFC%40cmu.edu.
>
> --
> 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/CAOvivQwTR4qK094%2Bkmgj%3D2547UxGgmbjW9k5MgLe%2Bne9xPef3w%40mail.gmail.com.

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

* RE: [HoTT] Identity versus equality
2020-05-06 19:31        Steve Awodey
@ 2020-05-06 20:30          Joyal, André
2020-05-06 22:52          Thorsten Altenkirch
1 sibling, 0 replies; 61+ messages in thread
From: Joyal, André @ 2020-05-06 20:30 UTC (permalink / raw)
To: Steve Awodey, Michael Shulman; +Cc: HomotopyT...@googlegroups.com

Dear Steve and Mike,

I guess we essentially agree.
The idea that the equality relation a=b depends on a choice of identification of a with b is fundamental.
In a sense, it has been around since a long time, but not formally recognized
except in ML type theory and possibly in category theory.

I am dreaming of a formal system in which the identity type Id(a,b)
is so natural, that it disappear by not been problematic.
How could we teach homotopy type theory to engineers?

André

________________________________________
From: Steve Awodey [awo...@cmu.edu]
Sent: Wednesday, May 06, 2020 3:31 PM
To: Michael Shulman
Subject: Re: [HoTT] Identity versus equality

I totally agree with you, Mike.

But I think Thorsten was pointing out (he will correct me if I’m wrong)
that a = b meaning “equals” is maybe not the same as “identity”?

and I do think that the terminology “identification” is good for the elements of this type, which traditionally was called the “identity type".

maybe the answer is to say that mathematics simply doesn’t deal with the “metaphysical" notion of “identity”, as distinct from equality.
we just use both words interchangeably for the single notion expressd by a = b, which is short for Id(a,b).

> On May 6, 2020, at 3:18 PM, Michael Shulman <shu...@sandiego.edu> wrote:
>
> As I've said before, I strongly disagree that the standard
> interpretation of "a=b" as meaning "a equals b" clashes in any way
> with its use to denote the identity type.  Almost without exception,
> whenever a mathematican working informally says "equals", that *must*
> be formalized as referring to the identity type.  Ask any
> mathematician on the street whether x+y=y+x for all natural numbers x
> and y, and they will say yes.  But this is false if = means judgmental
> equality.  Judgmental equality is a technical object of type theory
> that the "generic mathematician" is not aware of at all, so it cannot
> co-opt the standard notation "=" or word "equals" if we want "informal
> type theory" to be at all comprehensible to such readers.
>
>
> On Wed, May 6, 2020 at 12:01 PM Steve Awodey <awo...@cmu.edu> wrote:
>>
>> Dear Andre’ (and all),
>>
>> The sign a = b is pretty well established in mathematics as meaning “a equals b”,
>> which does indeed clash with our choice in the book to use it for the identity type,
>> and to call the elements of this type “identifications”.
>> Thorsten has rightly pointed out this clash.
>>
>> Although I am personally not eager to make any changes in our current terminology and/or notation,
>> I’m certainly glad to consider the possibiiy
>> (we did agree to return to this question at some point, so maybe this is it : - ).
>>
>> We need both symbols and words for two notions:
>>
>> - judgemental equality, currently a\equiv b,
>> - propositional equality, currently a = b, short for Id(a,b).
>>
>> There seems to be a proposal to revise this to something like:
>>
>> - judgemental equality: written a = b and pronounced “a equals b”,
>> - propositional equality, written maybe a \cong b, and pronunced ”a iso b”,
>> (the elements of this type are called “isos").
>>
>> Another (partial) option would be:
>>
>> - judgemental equality: written a = b and pronounced “a equals b”,
>> - propositional equality, written Id(a,b) and shortened somehow a ? b,
>> and pronunced ”a idenitfied with b”
>> (the elements of this type are called “identifications").
>>
>> Do either of these seem preferable?
>> Are there other proposals?
>> And how should one decide?
>>
>> Regards,
>>
>> Steve
>>
>>
>>
>>
>>
>> On May 6, 2020, at 12:02 PM, Joyal, André <joyal...@uqam.ca> wrote:
>>
>> Dear all,
>>
>> A few more thoughts.
>> We all agree that terminology and notation are important.
>>
>> I love the story of the equality sign = introduced by Robert Recorde (1512-1558).
>> "because no two things can be more equal than a pair of parallel lines".
>> It took more than a century before been universally adopted.
>> René Descartes (1596-1650) used a different symbol  in his work (something like \alpha).
>> We may ask why Recorde's notation won over Descartes's notation?
>> Of course, we may never know.
>> I dare to say that Recorde's notation was *better*.
>> Among other things, the equality sign = is symmetric:
>> the expression a=b and b=a are mirror image of each other.
>> Recorde's motive for introducing the notation was more about
>> convenience and aesthetic than about philosophy and history.
>> The notation was gradually adopted because it is simple and useful.
>> It was not because Recorde was a powerful academic,
>> since he eventually died in prison.
>>
>> There is something to learn from the history of the equality sign.
>> I guess that it can also applied to terminology.
>> A new notation or terminology has a good chance to be adopted universally
>> if it is simple and useful, but it may take time.
>>
>> André
>> ________________________________
>> Sent: Tuesday, May 05, 2020 4:47 AM
>> Subject: [HoTT] Identity versus equality
>>
>> The discussion yesterday provides a good occasion for me to pose a question I have long wanted to put to this list: is there a convention generally agreed upon in the HoTT-community for when (if ever) to use 'identity' instead of 'equality'?
>>
>> Here are some relevant data.
>>
>> A Germanic equivalent for 'identity' is 'sameness'.
>> A Germanic equivalent for 'equality' is 'likeness'.
>>
>> For Aristotle equality means sameness of quantity. This is how one must understand 'equal' in Euclid's Elements, where a triangle may have all sides equal (clearly, they cannot be identical). The axiom in the Elements that has given rise to the term 'Euclidean relation' and which is appealed to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'.
>>
>> In Diophantus's Arithmetica, on the other hand, the two terms of an equation are said to be equal, not identical, and this would become the standard terminology in algebra. For instance, the sign '=' was introduced by Robert Recorde as a sign of equality, not as a sign of identity. The explanation for this apparent discrepancy with the Aristotelian/Euclidean terminology might be that when dealing with numbers, equality just is identity, since for two numbers to be identical as to magnitude just is for them to be the same number. Aristotle says as much in Metaphysics M.7.
>>
>> Hilbert and Bernays might be one of the few logic books in the modern era to distinguish equality from identity (volume I, chapter 5). 'Equality' is there used for any equivalence relation and glossed as the obtaining of "irgendeine Art von Übereinstimmung". Identity, by contrast, is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility within the given language.
>>
>> Frege, by contrast, explicitly identifies (sic!) equality with identity, and glosses the latter as sameness or coincidence, in the first footnote to his paper on sense and reference.  Kleene and Church do the same in their famous textbooks: if one looks under 'identity' in the index to any of those books one is referred to 'equality'.
>>
>> Clearly the two cannot be assumed to mean the same by analysts who speak of two functions being identically equal!
>>
>> --
>> 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/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%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/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca.
>>
>>
>> --
>> 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/05375057-883F-4487-8919-2579F5771AFC%40cmu.edu.
>
> --
> 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/CAOvivQwTR4qK094%2Bkmgj%3D2547UxGgmbjW9k5MgLe%2Bne9xPef3w%40mail.gmail.com.

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

* Re: [HoTT] Identity versus equality
2020-05-06 19:31        Steve Awodey
2020-05-06 20:30          Joyal, André
@ 2020-05-06 22:52          Thorsten Altenkirch
1 sibling, 0 replies; 61+ messages in thread
From: Thorsten Altenkirch @ 2020-05-06 22:52 UTC (permalink / raw)
To: Steve Awodey, Michael Shulman

I always thought that equality and identity are synonyms. Sometimes we talk about equations and sometimes we call them identities. So yes, I agree completely.

Thorsten

﻿On 06/05/2020, 20:31, "homotopyt...@googlegroups.com on behalf of Steve Awodey" <homotopyt...@googlegroups.com on behalf of awo...@cmu.edu> wrote:

I totally agree with you, Mike.

But I think Thorsten was pointing out (he will correct me if I’m wrong)
that a = b meaning “equals” is maybe not the same as “identity”?

and I do think that the terminology “identification” is good for the elements of this type, which traditionally was called the “identity type".

maybe the answer is to say that mathematics simply doesn’t deal with the “metaphysical" notion of “identity”, as distinct from equality.
we just use both words interchangeably for the single notion expressd by a = b, which is short for Id(a,b).

> On May 6, 2020, at 3:18 PM, Michael Shulman <shu...@sandiego.edu> wrote:
>
> As I've said before, I strongly disagree that the standard
> interpretation of "a=b" as meaning "a equals b" clashes in any way
> with its use to denote the identity type.  Almost without exception,
> whenever a mathematican working informally says "equals", that *must*
> be formalized as referring to the identity type.  Ask any
> mathematician on the street whether x+y=y+x for all natural numbers x
> and y, and they will say yes.  But this is false if = means judgmental
> equality.  Judgmental equality is a technical object of type theory
> that the "generic mathematician" is not aware of at all, so it cannot
> co-opt the standard notation "=" or word "equals" if we want "informal
> type theory" to be at all comprehensible to such readers.
>
>
> On Wed, May 6, 2020 at 12:01 PM Steve Awodey <awo...@cmu.edu> wrote:
>>
>> Dear Andre’ (and all),
>>
>> The sign a = b is pretty well established in mathematics as meaning “a equals b”,
>> which does indeed clash with our choice in the book to use it for the identity type,
>> and to call the elements of this type “identifications”.
>> Thorsten has rightly pointed out this clash.
>>
>> Although I am personally not eager to make any changes in our current terminology and/or notation,
>> I’m certainly glad to consider the possibiiy
>> (we did agree to return to this question at some point, so maybe this is it : - ).
>>
>> We need both symbols and words for two notions:
>>
>> - judgemental equality, currently a\equiv b,
>> - propositional equality, currently a = b, short for Id(a,b).
>>
>> There seems to be a proposal to revise this to something like:
>>
>> - judgemental equality: written a = b and pronounced “a equals b”,
>> - propositional equality, written maybe a \cong b, and pronunced ”a iso b”,
>> (the elements of this type are called “isos").
>>
>> Another (partial) option would be:
>>
>> - judgemental equality: written a = b and pronounced “a equals b”,
>> - propositional equality, written Id(a,b) and shortened somehow a ? b,
>> and pronunced ”a idenitfied with b”
>> (the elements of this type are called “identifications").
>>
>> Do either of these seem preferable?
>> Are there other proposals?
>> And how should one decide?
>>
>> Regards,
>>
>> Steve
>>
>>
>>
>>
>>
>> On May 6, 2020, at 12:02 PM, Joyal, André <joyal...@uqam.ca> wrote:
>>
>> Dear all,
>>
>> A few more thoughts.
>> We all agree that terminology and notation are important.
>>
>> I love the story of the equality sign = introduced by Robert Recorde (1512-1558).
>> "because no two things can be more equal than a pair of parallel lines".
>> It took more than a century before been universally adopted.
>> René Descartes (1596-1650) used a different symbol  in his work (something like \alpha).
>> We may ask why Recorde's notation won over Descartes's notation?
>> Of course, we may never know.
>> I dare to say that Recorde's notation was *better*.
>> Among other things, the equality sign = is symmetric:
>> the expression a=b and b=a are mirror image of each other.
>> Recorde's motive for introducing the notation was more about
>> convenience and aesthetic than about philosophy and history.
>> The notation was gradually adopted because it is simple and useful.
>> It was not because Recorde was a powerful academic,
>> since he eventually died in prison.
>>
>> There is something to learn from the history of the equality sign.
>> I guess that it can also applied to terminology.
>> A new notation or terminology has a good chance to be adopted universally
>> if it is simple and useful, but it may take time.
>>
>> André
>> ________________________________
>> Sent: Tuesday, May 05, 2020 4:47 AM
>> Subject: [HoTT] Identity versus equality
>>
>> The discussion yesterday provides a good occasion for me to pose a question I have long wanted to put to this list: is there a convention generally agreed upon in the HoTT-community for when (if ever) to use 'identity' instead of 'equality'?
>>
>> Here are some relevant data.
>>
>> A Germanic equivalent for 'identity' is 'sameness'.
>> A Germanic equivalent for 'equality' is 'likeness'.
>>
>> For Aristotle equality means sameness of quantity. This is how one must understand 'equal' in Euclid's Elements, where a triangle may have all sides equal (clearly, they cannot be identical). The axiom in the Elements that has given rise to the term 'Euclidean relation' and which is appealed to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'.
>>
>> In Diophantus's Arithmetica, on the other hand, the two terms of an equation are said to be equal, not identical, and this would become the standard terminology in algebra. For instance, the sign '=' was introduced by Robert Recorde as a sign of equality, not as a sign of identity. The explanation for this apparent discrepancy with the Aristotelian/Euclidean terminology might be that when dealing with numbers, equality just is identity, since for two numbers to be identical as to magnitude just is for them to be the same number. Aristotle says as much in Metaphysics M.7.
>>
>> Hilbert and Bernays might be one of the few logic books in the modern era to distinguish equality from identity (volume I, chapter 5). 'Equality' is there used for any equivalence relation and glossed as the obtaining of "irgendeine Art von Übereinstimmung". Identity, by contrast, is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility within the given language.
>>
>> Frege, by contrast, explicitly identifies (sic!) equality with identity, and glosses the latter as sameness or coincidence, in the first footnote to his paper on sense and reference.  Kleene and Church do the same in their famous textbooks: if one looks under 'identity' in the index to any of those books one is referred to 'equality'.
>>
>> Clearly the two cannot be assumed to mean the same by analysts who speak of two functions being identically equal!
>>
>> --
>> 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/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%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/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca.
>>
>>
>> --
>> 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/05375057-883F-4487-8919-2579F5771AFC%40cmu.edu.
>
> --
> 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/CAOvivQwTR4qK094%2Bkmgj%3D2547UxGgmbjW9k5MgLe%2Bne9xPef3w%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/35D53A79-56C0-42F7-A58F-6052CE26FA87%40cmu.edu.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
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] 61+ messages in thread

* Re: [HoTT] Identity versus equality
2020-05-06 19:18      Michael Shulman
2020-05-06 19:31        Steve Awodey
@ 2020-05-06 22:54        Thorsten Altenkirch
2020-05-06 23:29          Joyal, André
From: Thorsten Altenkirch @ 2020-05-06 22:54 UTC (permalink / raw)
To: Michael Shulman, Steve Awodey

I agree but let me try to make this more precise. We cannot talk about judgemental equality within Mathematics it is not a proposition. Judgemental equality is important when we talk about Mathematics, it is a property of a mathematical text. The same applies to typing: we cannot talk about typing because it is not a proposition it is a part of the structure of our argument.

This becomes clear in the example: we talk about numbers but x+y is an expression, hence talking about judgemental equality only makes sense when we talk about Mathematics. To say that x+y is not judgemental equal to y+x doesn't make any sense within our argument it is a sentence about it.

When I say that 0+x is definitionally equal to x I don't prove anything but I just point out a fact that follows from the definition of +. That is I draw attention to it.

Hence clearly there is no reason to use any other word that equality to mean that two objects are equal which means that the equality type is inhabited which is signified by using =. There is the issue that we may have a more that one way in which two objects can be equal which creates the need to talk about elements of an equality type. 	I don't like the word "identifications" because it seems to suggest that the two objects are not properly equal but just "identified" artificially.

Thorsten

﻿On 06/05/2020, 20:19, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> wrote:

As I've said before, I strongly disagree that the standard
interpretation of "a=b" as meaning "a equals b" clashes in any way
with its use to denote the identity type.  Almost without exception,
whenever a mathematican working informally says "equals", that *must*
be formalized as referring to the identity type.  Ask any
mathematician on the street whether x+y=y+x for all natural numbers x
and y, and they will say yes.  But this is false if = means judgmental
equality.  Judgmental equality is a technical object of type theory
that the "generic mathematician" is not aware of at all, so it cannot
co-opt the standard notation "=" or word "equals" if we want "informal
type theory" to be at all comprehensible to such readers.

On Wed, May 6, 2020 at 12:01 PM Steve Awodey <awo...@cmu.edu> wrote:
>
> Dear Andre’ (and all),
>
> The sign a = b is pretty well established in mathematics as meaning “a equals b”,
> which does indeed clash with our choice in the book to use it for the identity type,
> and to call the elements of this type “identifications”.
> Thorsten has rightly pointed out this clash.
>
> Although I am personally not eager to make any changes in our current terminology and/or notation,
> I’m certainly glad to consider the possibiiy
> (we did agree to return to this question at some point, so maybe this is it : - ).
>
> We need both symbols and words for two notions:
>
> - judgemental equality, currently a\equiv b,
> - propositional equality, currently a = b, short for Id(a,b).
>
> There seems to be a proposal to revise this to something like:
>
> - judgemental equality: written a = b and pronounced “a equals b”,
> - propositional equality, written maybe a \cong b, and pronunced ”a iso b”,
> (the elements of this type are called “isos").
>
> Another (partial) option would be:
>
> - judgemental equality: written a = b and pronounced “a equals b”,
> - propositional equality, written Id(a,b) and shortened somehow a ? b,
> and pronunced ”a idenitfied with b”
> (the elements of this type are called “identifications").
>
> Do either of these seem preferable?
> Are there other proposals?
> And how should one decide?
>
> Regards,
>
> Steve
>
>
>
>
>
> On May 6, 2020, at 12:02 PM, Joyal, André <joyal...@uqam.ca> wrote:
>
> Dear all,
>
> A few more thoughts.
> We all agree that terminology and notation are important.
>
> I love the story of the equality sign = introduced by Robert Recorde (1512-1558).
> "because no two things can be more equal than a pair of parallel lines".
> It took more than a century before been universally adopted.
> René Descartes (1596-1650) used a different symbol  in his work (something like \alpha).
> We may ask why Recorde's notation won over Descartes's notation?
> Of course, we may never know.
> I dare to say that Recorde's notation was *better*.
> Among other things, the equality sign = is symmetric:
> the expression a=b and b=a are mirror image of each other.
> Recorde's motive for introducing the notation was more about
> convenience and aesthetic than about philosophy and history.
> The notation was gradually adopted because it is simple and useful.
> It was not because Recorde was a powerful academic,
> since he eventually died in prison.
>
> There is something to learn from the history of the equality sign.
> I guess that it can also applied to terminology.
> A new notation or terminology has a good chance to be adopted universally
> if it is simple and useful, but it may take time.
>
> André
> ________________________________
> Sent: Tuesday, May 05, 2020 4:47 AM
> Subject: [HoTT] Identity versus equality
>
> The discussion yesterday provides a good occasion for me to pose a question I have long wanted to put to this list: is there a convention generally agreed upon in the HoTT-community for when (if ever) to use 'identity' instead of 'equality'?
>
> Here are some relevant data.
>
> A Germanic equivalent for 'identity' is 'sameness'.
> A Germanic equivalent for 'equality' is 'likeness'.
>
> For Aristotle equality means sameness of quantity. This is how one must understand 'equal' in Euclid's Elements, where a triangle may have all sides equal (clearly, they cannot be identical). The axiom in the Elements that has given rise to the term 'Euclidean relation' and which is appealed to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'.
>
> In Diophantus's Arithmetica, on the other hand, the two terms of an equation are said to be equal, not identical, and this would become the standard terminology in algebra. For instance, the sign '=' was introduced by Robert Recorde as a sign of equality, not as a sign of identity. The explanation for this apparent discrepancy with the Aristotelian/Euclidean terminology might be that when dealing with numbers, equality just is identity, since for two numbers to be identical as to magnitude just is for them to be the same number. Aristotle says as much in Metaphysics M.7.
>
> Hilbert and Bernays might be one of the few logic books in the modern era to distinguish equality from identity (volume I, chapter 5). 'Equality' is there used for any equivalence relation and glossed as the obtaining of "irgendeine Art von Übereinstimmung". Identity, by contrast, is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility within the given language.
>
> Frege, by contrast, explicitly identifies (sic!) equality with identity, and glosses the latter as sameness or coincidence, in the first footnote to his paper on sense and reference.  Kleene and Church do the same in their famous textbooks: if one looks under 'identity' in the index to any of those books one is referred to 'equality'.
>
> Clearly the two cannot be assumed to mean the same by analysts who speak of two functions being identically equal!
>
> --
> 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/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%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/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca.
>
>
> --
> 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/05375057-883F-4487-8919-2579F5771AFC%40cmu.edu.

--
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/CAOvivQwTR4qK094%2Bkmgj%3D2547UxGgmbjW9k5MgLe%2Bne9xPef3w%40mail.gmail.com.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
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] 61+ messages in thread

* RE: [HoTT] Identity versus equality
2020-05-06 22:54        Thorsten Altenkirch
@ 2020-05-06 23:29          Joyal, André
2020-05-07  6:11            Egbert Rijke
2020-05-07  6:58            Thorsten Altenkirch
0 siblings, 2 replies; 61+ messages in thread
From: Joyal, André @ 2020-05-06 23:29 UTC (permalink / raw)
To: Thorsten Altenkirch, Michael Shulman, Steve Awodey

Dear Thorsten,

I have naive question for experts.

I believe that judgemental equality is on the syntactic side of type theory,
while propositional equality is on the semantical side.
The homotopical interpretation of type theory is mainly
concerned with propositional equality.
What is the semantic of judgemental equality?
(independantly of the semantic of propositional equality).
Could we reverse the role of the two equalities?
Could we regard judgemental equality as the true meaning
of type theory, while regarding propositional equality
as a purely formal game?

André

________________________________________
From: Thorsten Altenkirch [Thorsten....@nottingham.ac.uk]
Sent: Wednesday, May 06, 2020 6:54 PM
To: Michael Shulman; Steve Awodey
Subject: Re: [HoTT] Identity versus equality

I agree but let me try to make this more precise. We cannot talk about judgemental equality within Mathematics it is not a proposition. Judgemental equality is important when we talk about Mathematics, it is a property of a mathematical text. The same applies to typing: we cannot talk about typing because it is not a proposition it is a part of the structure of our argument.

This becomes clear in the example: we talk about numbers but x+y is an expression, hence talking about judgemental equality only makes sense when we talk about Mathematics. To say that x+y is not judgemental equal to y+x doesn't make any sense within our argument it is a sentence about it.

When I say that 0+x is definitionally equal to x I don't prove anything but I just point out a fact that follows from the definition of +. That is I draw attention to it.

Hence clearly there is no reason to use any other word that equality to mean that two objects are equal which means that the equality type is inhabited which is signified by using =. There is the issue that we may have a more that one way in which two objects can be equal which creates the need to talk about elements of an equality type.     I don't like the word "identifications" because it seems to suggest that the two objects are not properly equal but just "identified" artificially.

Thorsten

﻿On 06/05/2020, 20:19, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> wrote:

As I've said before, I strongly disagree that the standard
interpretation of "a=b" as meaning "a equals b" clashes in any way
with its use to denote the identity type.  Almost without exception,
whenever a mathematican working informally says "equals", that *must*
be formalized as referring to the identity type.  Ask any
mathematician on the street whether x+y=y+x for all natural numbers x
and y, and they will say yes.  But this is false if = means judgmental
equality.  Judgmental equality is a technical object of type theory
that the "generic mathematician" is not aware of at all, so it cannot
co-opt the standard notation "=" or word "equals" if we want "informal
type theory" to be at all comprehensible to such readers.

On Wed, May 6, 2020 at 12:01 PM Steve Awodey <awo...@cmu.edu> wrote:
>
> Dear Andre’ (and all),
>
> The sign a = b is pretty well established in mathematics as meaning “a equals b”,
> which does indeed clash with our choice in the book to use it for the identity type,
> and to call the elements of this type “identifications”.
> Thorsten has rightly pointed out this clash.
>
> Although I am personally not eager to make any changes in our current terminology and/or notation,
> I’m certainly glad to consider the possibiiy
> (we did agree to return to this question at some point, so maybe this is it : - ).
>
> We need both symbols and words for two notions:
>
> - judgemental equality, currently a\equiv b,
> - propositional equality, currently a = b, short for Id(a,b).
>
> There seems to be a proposal to revise this to something like:
>
> - judgemental equality: written a = b and pronounced “a equals b”,
> - propositional equality, written maybe a \cong b, and pronunced ”a iso b”,
> (the elements of this type are called “isos").
>
> Another (partial) option would be:
>
> - judgemental equality: written a = b and pronounced “a equals b”,
> - propositional equality, written Id(a,b) and shortened somehow a ? b,
> and pronunced ”a idenitfied with b”
> (the elements of this type are called “identifications").
>
> Do either of these seem preferable?
> Are there other proposals?
> And how should one decide?
>
> Regards,
>
> Steve
>
>
>
>
>
> On May 6, 2020, at 12:02 PM, Joyal, André <joyal...@uqam.ca> wrote:
>
> Dear all,
>
> A few more thoughts.
> We all agree that terminology and notation are important.
>
> I love the story of the equality sign = introduced by Robert Recorde (1512-1558).
> "because no two things can be more equal than a pair of parallel lines".
> It took more than a century before been universally adopted.
> René Descartes (1596-1650) used a different symbol  in his work (something like \alpha).
> We may ask why Recorde's notation won over Descartes's notation?
> Of course, we may never know.
> I dare to say that Recorde's notation was *better*.
> Among other things, the equality sign = is symmetric:
> the expression a=b and b=a are mirror image of each other.
> Recorde's motive for introducing the notation was more about
> convenience and aesthetic than about philosophy and history.
> The notation was gradually adopted because it is simple and useful.
> It was not because Recorde was a powerful academic,
> since he eventually died in prison.
>
> There is something to learn from the history of the equality sign.
> I guess that it can also applied to terminology.
> A new notation or terminology has a good chance to be adopted universally
> if it is simple and useful, but it may take time.
>
> André
> ________________________________
> Sent: Tuesday, May 05, 2020 4:47 AM
> Subject: [HoTT] Identity versus equality
>
> The discussion yesterday provides a good occasion for me to pose a question I have long wanted to put to this list: is there a convention generally agreed upon in the HoTT-community for when (if ever) to use 'identity' instead of 'equality'?
>
> Here are some relevant data.
>
> A Germanic equivalent for 'identity' is 'sameness'.
> A Germanic equivalent for 'equality' is 'likeness'.
>
> For Aristotle equality means sameness of quantity. This is how one must understand 'equal' in Euclid's Elements, where a triangle may have all sides equal (clearly, they cannot be identical). The axiom in the Elements that has given rise to the term 'Euclidean relation' and which is appealed to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'.
>
> In Diophantus's Arithmetica, on the other hand, the two terms of an equation are said to be equal, not identical, and this would become the standard terminology in algebra. For instance, the sign '=' was introduced by Robert Recorde as a sign of equality, not as a sign of identity. The explanation for this apparent discrepancy with the Aristotelian/Euclidean terminology might be that when dealing with numbers, equality just is identity, since for two numbers to be identical as to magnitude just is for them to be the same number. Aristotle says as much in Metaphysics M.7.
>
> Hilbert and Bernays might be one of the few logic books in the modern era to distinguish equality from identity (volume I, chapter 5). 'Equality' is there used for any equivalence relation and glossed as the obtaining of "irgendeine Art von Übereinstimmung". Identity, by contrast, is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility within the given language.
>
> Frege, by contrast, explicitly identifies (sic!) equality with identity, and glosses the latter as sameness or coincidence, in the first footnote to his paper on sense and reference.  Kleene and Church do the same in their famous textbooks: if one looks under 'identity' in the index to any of those books one is referred to 'equality'.
>
> Clearly the two cannot be assumed to mean the same by analysts who speak of two functions being identically equal!
>
> --
> 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/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%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/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca.
>
>
> --
> 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/05375057-883F-4487-8919-2579F5771AFC%40cmu.edu.

--
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/CAOvivQwTR4qK094%2Bkmgj%3D2547UxGgmbjW9k5MgLe%2Bne9xPef3w%40mail.gmail.com.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
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] 61+ messages in thread

* Re: [HoTT] Identity versus equality
2020-05-06 23:29          Joyal, André
@ 2020-05-07  6:11            Egbert Rijke
2020-05-07  6:58            Thorsten Altenkirch
1 sibling, 0 replies; 61+ messages in thread
From: Egbert Rijke @ 2020-05-07  6:11 UTC (permalink / raw)
To: Joyal, André
Cc: Thorsten Altenkirch, Michael Shulman, Steve Awodey,

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

Dear all,

Perhaps I would say that judgmental equality is even more on the semantic
side than the identity type. We can reason about the identity type within
type theory, but we can only reason about judgmental equality when we're
considering semantics for type theory. For example, when you study
dependent type theory as an essentially algebraic theory, and want to know
what equalities hold in the algebras for that theory, then you're studying
judgmental equality. It has been said a few times that we cannot talk about
judgmental equality in mathematics, but I disagree. When we do semantics of
type theory we *have to* talk about judgmental equality, and of course
there is nothing that stops us from doing so.

With kind regards,
Egbert

On Thu, May 7, 2020 at 1:29 AM Joyal, André <joyal...@uqam.ca> wrote:

> Dear Thorsten,
>
> I have naive question for experts.
>
> I believe that judgemental equality is on the syntactic side of type
> theory,
> while propositional equality is on the semantical side.
> The homotopical interpretation of type theory is mainly
> concerned with propositional equality.
> What is the semantic of judgemental equality?
> (independantly of the semantic of propositional equality).
> Could we reverse the role of the two equalities?
> Could we regard judgemental equality as the true meaning
> of type theory, while regarding propositional equality
> as a purely formal game?
>
> André
>
>
>
>
>
> ________________________________________
> From: Thorsten Altenkirch [Thorsten....@nottingham.ac.uk]
> Sent: Wednesday, May 06, 2020 6:54 PM
> To: Michael Shulman; Steve Awodey
> Subject: Re: [HoTT] Identity versus equality
>
> I agree but let me try to make this more precise. We cannot talk about
> judgemental equality within Mathematics it is not a proposition.
> Judgemental equality is important when we talk about Mathematics, it is a
> property of a mathematical text. The same applies to typing: we cannot talk
> about typing because it is not a proposition it is a part of the structure
> of our argument.
>
> This becomes clear in the example: we talk about numbers but x+y is an
> expression, hence talking about judgemental equality only makes sense when
> we talk about Mathematics. To say that x+y is not judgemental equal to y+x
> doesn't make any sense within our argument it is a sentence about it.
>
> When I say that 0+x is definitionally equal to x I don't prove anything
> but I just point out a fact that follows from the definition of +. That is
> I draw attention to it.
>
> Hence clearly there is no reason to use any other word that equality to
> mean that two objects are equal which means that the equality type is
> inhabited which is signified by using =. There is the issue that we may
> have a more that one way in which two objects can be equal which creates
> the need to talk about elements of an equality type.     I don't like the
> word "identifications" because it seems to suggest that the two objects are
> not properly equal but just "identified" artificially.
>
> Thorsten
>
> ﻿On 06/05/2020, 20:19, "homotopyt...@googlegroups.com on behalf of
> Michael Shulman" <homotopyt...@googlegroups.com on behalf of
> shu...@sandiego.edu> wrote:
>
>     As I've said before, I strongly disagree that the standard
>     interpretation of "a=b" as meaning "a equals b" clashes in any way
>     with its use to denote the identity type.  Almost without exception,
>     whenever a mathematican working informally says "equals", that *must*
>     be formalized as referring to the identity type.  Ask any
>     mathematician on the street whether x+y=y+x for all natural numbers x
>     and y, and they will say yes.  But this is false if = means judgmental
>     equality.  Judgmental equality is a technical object of type theory
>     that the "generic mathematician" is not aware of at all, so it cannot
>     co-opt the standard notation "=" or word "equals" if we want "informal
>     type theory" to be at all comprehensible to such readers.
>
>
>     On Wed, May 6, 2020 at 12:01 PM Steve Awodey <awo...@cmu.edu> wrote:
>     >
>     > Dear Andre’ (and all),
>     >
>     > The sign a = b is pretty well established in mathematics as meaning
> “a equals b”,
>     > which does indeed clash with our choice in the book to use it for
> the identity type,
>     > and to call the elements of this type “identifications”.
>     > Thorsten has rightly pointed out this clash.
>     >
>     > Although I am personally not eager to make any changes in our
> current terminology and/or notation,
>     > I’m certainly glad to consider the possibiiy
>     > (we did agree to return to this question at some point, so maybe
> this is it : - ).
>     >
>     > We need both symbols and words for two notions:
>     >
>     > - judgemental equality, currently a\equiv b,
>     > - propositional equality, currently a = b, short for Id(a,b).
>     >
>     > There seems to be a proposal to revise this to something like:
>     >
>     > - judgemental equality: written a = b and pronounced “a equals b”,
>     > - propositional equality, written maybe a \cong b, and pronunced ”a
> iso b”,
>     > (the elements of this type are called “isos").
>     >
>     > Another (partial) option would be:
>     >
>     > - judgemental equality: written a = b and pronounced “a equals b”,
>     > - propositional equality, written Id(a,b) and shortened somehow a ?
> b,
>     > and pronunced ”a idenitfied with b”
>     > (the elements of this type are called “identifications").
>     >
>     > Do either of these seem preferable?
>     > Are there other proposals?
>     > And how should one decide?
>     >
>     > Regards,
>     >
>     > Steve
>     >
>     >
>     >
>     >
>     >
>     > On May 6, 2020, at 12:02 PM, Joyal, André <joyal...@uqam.ca>
> wrote:
>     >
>     > Dear all,
>     >
>     > A few more thoughts.
>     > We all agree that terminology and notation are important.
>     >
>     > I love the story of the equality sign = introduced by Robert Recorde
> (1512-1558).
>     > "because no two things can be more equal than a pair of parallel
> lines".
>     > It took more than a century before been universally adopted.
>     > René Descartes (1596-1650) used a different symbol  in his work
> (something like \alpha).
>     > We may ask why Recorde's notation won over Descartes's notation?
>     > Of course, we may never know.
>     > I dare to say that Recorde's notation was *better*.
>     > Among other things, the equality sign = is symmetric:
>     > the expression a=b and b=a are mirror image of each other.
>     > Recorde's motive for introducing the notation was more about
>     > convenience and aesthetic than about philosophy and history.
>     > The notation was gradually adopted because it is simple and useful.
>     > It was not because Recorde was a powerful academic,
>     > since he eventually died in prison.
>     >
>     > There is something to learn from the history of the equality sign.
>     > I guess that it can also applied to terminology.
>     > A new notation or terminology has a good chance to be adopted
> universally
>     > if it is simple and useful, but it may take time.
>     >
>     > André
>     > ________________________________
> homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [
> anste...@gmail.com]
>     > Sent: Tuesday, May 05, 2020 4:47 AM
>     > Subject: [HoTT] Identity versus equality
>     >
>     > The discussion yesterday provides a good occasion for me to pose a
> question I have long wanted to put to this list: is there a convention
> generally agreed upon in the HoTT-community for when (if ever) to use
>     >
>     > Here are some relevant data.
>     >
>     > A Germanic equivalent for 'identity' is 'sameness'.
>     > A Germanic equivalent for 'equality' is 'likeness'.
>     >
>     > For Aristotle equality means sameness of quantity. This is how one
> must understand 'equal' in Euclid's Elements, where a triangle may have all
> sides equal (clearly, they cannot be identical). The axiom in the Elements
> that has given rise to the term 'Euclidean relation' and which is appealed
> to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'.
>     >
>     > In Diophantus's Arithmetica, on the other hand, the two terms of an
> equation are said to be equal, not identical, and this would become the
> standard terminology in algebra. For instance, the sign '=' was introduced
> by Robert Recorde as a sign of equality, not as a sign of identity. The
> explanation for this apparent discrepancy with the Aristotelian/Euclidean
> terminology might be that when dealing with numbers, equality just is
> identity, since for two numbers to be identical as to magnitude just is for
> them to be the same number. Aristotle says as much in Metaphysics M.7.
>     >
>     > Hilbert and Bernays might be one of the few logic books in the
> modern era to distinguish equality from identity (volume I, chapter 5).
> 'Equality' is there used for any equivalence relation and glossed as the
> obtaining of "irgendeine Art von Übereinstimmung". Identity, by contrast,
> is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility
> within the given language.
>     >
>     > Frege, by contrast, explicitly identifies (sic!) equality with
> identity, and glosses the latter as sameness or coincidence, in the first
> footnote to his paper on sense and reference.  Kleene and Church do the
> same in their famous textbooks: if one looks under 'identity' in the index
> to any of those books one is referred to 'equality'.
>     >
>     > Clearly the two cannot be assumed to mean the same by analysts who
> speak of two functions being identically equal!
>     >
>     > --
>     > 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
> .
>     >
>     > --
>     > 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
> .
>     >
>     >
>     > --
>     > 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
> .
>
>     --
>     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
>     To view this discussion on the web visit
> .
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> 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
> To view this discussion on the web visit
> .
>

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

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

* Re: [HoTT] Identity versus equality
2020-05-06 23:29          Joyal, André
2020-05-07  6:11            Egbert Rijke
@ 2020-05-07  6:58            Thorsten Altenkirch
2020-05-07  9:04              Ansten Mørch Klev
2020-05-07 10:09              Thomas Streicher
1 sibling, 2 replies; 61+ messages in thread
From: Thorsten Altenkirch @ 2020-05-07  6:58 UTC (permalink / raw)
To: Joyal, André, Michael Shulman, Steve Awodey

Dear Andre,

It seems that Egbert already gave the perfect answer. When we about Type Theory we don't only talk about syntax but about the relation of syntax and semantics. And then judgemental equality is modelled by propositional equality in the metatheory. Not a reversal but a level shift.

I wouldn't say that propositional equality is a purely formal game, indeed we explain the nature of equality by modelling it. In a set theoretic setting it is enough to say that equality is a congruence, i.e. an equivalence relation that is preserved by all functions. But this is not sufficient to explain structural equality which is not propositional. As you know best (because you have invented many of the important notions) a better explanation of equality is that is an omega groupoid and that all functions are modelled as functors on these groupoids.

Cheers,
Thorsten

﻿On 07/05/2020, 00:29, "Joyal, André" <joyal...@uqam.ca> wrote:

Dear Thorsten,

I have naive question for experts.

I believe that judgemental equality is on the syntactic side of type theory,
while propositional equality is on the semantical side.
The homotopical interpretation of type theory is mainly
concerned with propositional equality.
What is the semantic of judgemental equality?
(independantly of the semantic of propositional equality).
Could we reverse the role of the two equalities?
Could we regard judgemental equality as the true meaning
of type theory, while regarding propositional equality
as a purely formal game?

André

________________________________________
From: Thorsten Altenkirch [Thorsten....@nottingham.ac.uk]
Sent: Wednesday, May 06, 2020 6:54 PM
To: Michael Shulman; Steve Awodey
Subject: Re: [HoTT] Identity versus equality

I agree but let me try to make this more precise. We cannot talk about judgemental equality within Mathematics it is not a proposition. Judgemental equality is important when we talk about Mathematics, it is a property of a mathematical text. The same applies to typing: we cannot talk about typing because it is not a proposition it is a part of the structure of our argument.

This becomes clear in the example: we talk about numbers but x+y is an expression, hence talking about judgemental equality only makes sense when we talk about Mathematics. To say that x+y is not judgemental equal to y+x doesn't make any sense within our argument it is a sentence about it.

When I say that 0+x is definitionally equal to x I don't prove anything but I just point out a fact that follows from the definition of +. That is I draw attention to it.

Hence clearly there is no reason to use any other word that equality to mean that two objects are equal which means that the equality type is inhabited which is signified by using =. There is the issue that we may have a more that one way in which two objects can be equal which creates the need to talk about elements of an equality type.     I don't like the word "identifications" because it seems to suggest that the two objects are not properly equal but just "identified" artificially.

Thorsten

On 06/05/2020, 20:19, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> wrote:

As I've said before, I strongly disagree that the standard
interpretation of "a=b" as meaning "a equals b" clashes in any way
with its use to denote the identity type.  Almost without exception,
whenever a mathematican working informally says "equals", that *must*
be formalized as referring to the identity type.  Ask any
mathematician on the street whether x+y=y+x for all natural numbers x
and y, and they will say yes.  But this is false if = means judgmental
equality.  Judgmental equality is a technical object of type theory
that the "generic mathematician" is not aware of at all, so it cannot
co-opt the standard notation "=" or word "equals" if we want "informal
type theory" to be at all comprehensible to such readers.

On Wed, May 6, 2020 at 12:01 PM Steve Awodey <awo...@cmu.edu> wrote:
>
> Dear Andre’ (and all),
>
> The sign a = b is pretty well established in mathematics as meaning “a equals b”,
> which does indeed clash with our choice in the book to use it for the identity type,
> and to call the elements of this type “identifications”.
> Thorsten has rightly pointed out this clash.
>
> Although I am personally not eager to make any changes in our current terminology and/or notation,
> I’m certainly glad to consider the possibiiy
> (we did agree to return to this question at some point, so maybe this is it : - ).
>
> We need both symbols and words for two notions:
>
> - judgemental equality, currently a\equiv b,
> - propositional equality, currently a = b, short for Id(a,b).
>
> There seems to be a proposal to revise this to something like:
>
> - judgemental equality: written a = b and pronounced “a equals b”,
> - propositional equality, written maybe a \cong b, and pronunced ”a iso b”,
> (the elements of this type are called “isos").
>
> Another (partial) option would be:
>
> - judgemental equality: written a = b and pronounced “a equals b”,
> - propositional equality, written Id(a,b) and shortened somehow a ? b,
> and pronunced ”a idenitfied with b”
> (the elements of this type are called “identifications").
>
> Do either of these seem preferable?
> Are there other proposals?
> And how should one decide?
>
> Regards,
>
> Steve
>
>
>
>
>
> On May 6, 2020, at 12:02 PM, Joyal, André <joyal...@uqam.ca> wrote:
>
> Dear all,
>
> A few more thoughts.
> We all agree that terminology and notation are important.
>
> I love the story of the equality sign = introduced by Robert Recorde (1512-1558).
> "because no two things can be more equal than a pair of parallel lines".
> It took more than a century before been universally adopted.
> René Descartes (1596-1650) used a different symbol  in his work (something like \alpha).
> We may ask why Recorde's notation won over Descartes's notation?
> Of course, we may never know.
> I dare to say that Recorde's notation was *better*.
> Among other things, the equality sign = is symmetric:
> the expression a=b and b=a are mirror image of each other.
> Recorde's motive for introducing the notation was more about
> convenience and aesthetic than about philosophy and history.
> The notation was gradually adopted because it is simple and useful.
> It was not because Recorde was a powerful academic,
> since he eventually died in prison.
>
> There is something to learn from the history of the equality sign.
> I guess that it can also applied to terminology.
> A new notation or terminology has a good chance to be adopted universally
> if it is simple and useful, but it may take time.
>
> André
> ________________________________
> Sent: Tuesday, May 05, 2020 4:47 AM
> Subject: [HoTT] Identity versus equality
>
> The discussion yesterday provides a good occasion for me to pose a question I have long wanted to put to this list: is there a convention generally agreed upon in the HoTT-community for when (if ever) to use 'identity' instead of 'equality'?
>
> Here are some relevant data.
>
> A Germanic equivalent for 'identity' is 'sameness'.
> A Germanic equivalent for 'equality' is 'likeness'.
>
> For Aristotle equality means sameness of quantity. This is how one must understand 'equal' in Euclid's Elements, where a triangle may have all sides equal (clearly, they cannot be identical). The axiom in the Elements that has given rise to the term 'Euclidean relation' and which is appealed to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'.
>
> In Diophantus's Arithmetica, on the other hand, the two terms of an equation are said to be equal, not identical, and this would become the standard terminology in algebra. For instance, the sign '=' was introduced by Robert Recorde as a sign of equality, not as a sign of identity. The explanation for this apparent discrepancy with the Aristotelian/Euclidean terminology might be that when dealing with numbers, equality just is identity, since for two numbers to be identical as to magnitude just is for them to be the same number. Aristotle says as much in Metaphysics M.7.
>
> Hilbert and Bernays might be one of the few logic books in the modern era to distinguish equality from identity (volume I, chapter 5). 'Equality' is there used for any equivalence relation and glossed as the obtaining of "irgendeine Art von Übereinstimmung". Identity, by contrast, is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility within the given language.
>
> Frege, by contrast, explicitly identifies (sic!) equality with identity, and glosses the latter as sameness or coincidence, in the first footnote to his paper on sense and reference.  Kleene and Church do the same in their famous textbooks: if one looks under 'identity' in the index to any of those books one is referred to 'equality'.
>
> Clearly the two cannot be assumed to mean the same by analysts who speak of two functions being identically equal!
>
> --
> 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/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%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/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca.
>
>
> --
> 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/05375057-883F-4487-8919-2579F5771AFC%40cmu.edu.

--
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/CAOvivQwTR4qK094%2Bkmgj%3D2547UxGgmbjW9k5MgLe%2Bne9xPef3w%40mail.gmail.com.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
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.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
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] 61+ messages in thread

* Re: [HoTT] Identity versus equality
2020-05-07  6:58            Thorsten Altenkirch
@ 2020-05-07  9:04              Ansten Mørch Klev
2020-05-07 10:09              Thomas Streicher
1 sibling, 0 replies; 61+ messages in thread
From: Ansten Mørch Klev @ 2020-05-07  9:04 UTC (permalink / raw)
To: Thorsten Altenkirch
Cc: Joyal, André,

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

Dear all,

Thank you for your answers and for the stimulating discussion so far. I
agree that identity, to the extent that it is distinguished from equality,
is more of a philosopher's concept. One could perhaps say that in
mathematical logic there is an overlap of two terminological traditions: a
philosophical one, in which "identity" and "equality" are distinguished,
and a mathematical one, where they are not.

Regarding judgemental equality/identity: if by this one understands
definitional identity, then a case can be made that it is found also
outside type theory. Namely, instead of saying that a and b are
definitionally identical, we can also say that they are identical by
definition. And this phrase, "identical by definition", could well be used
by a "generic mathematician", could it not?
There is also the common practice of using a special identity sign when
writing definitions. One might say that the notion of definitional identity
captures the semantics of this special sign.

With kind regards,
Ansten Klev

On Thu, May 7, 2020 at 8:58 AM Thorsten Altenkirch <
Thorsten....@nottingham.ac.uk> wrote:

> Dear Andre,
>
> Theory we don't only talk about syntax but about the relation of syntax and
> semantics. And then judgemental equality is modelled by propositional
> equality in the metatheory. Not a reversal but a level shift.
>
> I wouldn't say that propositional equality is a purely formal game, indeed
> we explain the nature of equality by modelling it. In a set theoretic
> setting it is enough to say that equality is a congruence, i.e. an
> equivalence relation that is preserved by all functions. But this is not
> sufficient to explain structural equality which is not propositional. As
> you know best (because you have invented many of the important notions) a
> better explanation of equality is that is an omega groupoid and that all
> functions are modelled as functors on these groupoids.
>
> Cheers,
> Thorsten
>
> ﻿On 07/05/2020, 00:29, "Joyal, André" <joyal...@uqam.ca> wrote:
>
>     Dear Thorsten,
>
>     I have naive question for experts.
>
>     I believe that judgemental equality is on the syntactic side of type
> theory,
>     while propositional equality is on the semantical side.
>     The homotopical interpretation of type theory is mainly
>     concerned with propositional equality.
>     What is the semantic of judgemental equality?
>     (independantly of the semantic of propositional equality).
>     Could we reverse the role of the two equalities?
>     Could we regard judgemental equality as the true meaning
>     of type theory, while regarding propositional equality
>     as a purely formal game?
>
>     André
>
>
>
>
>
>     ________________________________________
>     From: Thorsten Altenkirch [Thorsten....@nottingham.ac.uk]
>     Sent: Wednesday, May 06, 2020 6:54 PM
>     To: Michael Shulman; Steve Awodey
>     Subject: Re: [HoTT] Identity versus equality
>
>     I agree but let me try to make this more precise. We cannot talk about
> judgemental equality within Mathematics it is not a proposition.
> Judgemental equality is important when we talk about Mathematics, it is a
> property of a mathematical text. The same applies to typing: we cannot talk
> about typing because it is not a proposition it is a part of the structure
> of our argument.
>
>     This becomes clear in the example: we talk about numbers but x+y is an
> expression, hence talking about judgemental equality only makes sense when
> we talk about Mathematics. To say that x+y is not judgemental equal to y+x
> doesn't make any sense within our argument it is a sentence about it.
>
>     When I say that 0+x is definitionally equal to x I don't prove
> anything but I just point out a fact that follows from the definition of +.
> That is I draw attention to it.
>
>     Hence clearly there is no reason to use any other word that equality
> to mean that two objects are equal which means that the equality type is
> inhabited which is signified by using =. There is the issue that we may
> have a more that one way in which two objects can be equal which creates
> the need to talk about elements of an equality type.     I don't like the
> word "identifications" because it seems to suggest that the two objects are
> not properly equal but just "identified" artificially.
>
>     Thorsten
>
>     On 06/05/2020, 20:19, "homotopyt...@googlegroups.com on behalf
> of Michael Shulman" <homotopyt...@googlegroups.com on behalf of
> shu...@sandiego.edu> wrote:
>
>         As I've said before, I strongly disagree that the standard
>         interpretation of "a=b" as meaning "a equals b" clashes in any way
>         with its use to denote the identity type.  Almost without
> exception,
>         whenever a mathematican working informally says "equals", that
> *must*
>         be formalized as referring to the identity type.  Ask any
>         mathematician on the street whether x+y=y+x for all natural
> numbers x
>         and y, and they will say yes.  But this is false if = means
> judgmental
>         equality.  Judgmental equality is a technical object of type theory
>         that the "generic mathematician" is not aware of at all, so it
> cannot
>         co-opt the standard notation "=" or word "equals" if we want
> "informal
>         type theory" to be at all comprehensible to such readers.
>
>
>         On Wed, May 6, 2020 at 12:01 PM Steve Awodey <awo...@cmu.edu>
> wrote:
>         >
>         > Dear Andre’ (and all),
>         >
>         > The sign a = b is pretty well established in mathematics as
> meaning “a equals b”,
>         > which does indeed clash with our choice in the book to use it
> for the identity type,
>         > and to call the elements of this type “identifications”.
>         > Thorsten has rightly pointed out this clash.
>         >
>         > Although I am personally not eager to make any changes in our
> current terminology and/or notation,
>         > I’m certainly glad to consider the possibiiy
>         > (we did agree to return to this question at some point, so maybe
> this is it : - ).
>         >
>         > We need both symbols and words for two notions:
>         >
>         > - judgemental equality, currently a\equiv b,
>         > - propositional equality, currently a = b, short for Id(a,b).
>         >
>         > There seems to be a proposal to revise this to something like:
>         >
>         > - judgemental equality: written a = b and pronounced “a equals
> b”,
>         > - propositional equality, written maybe a \cong b, and pronunced
> ”a iso b”,
>         > (the elements of this type are called “isos").
>         >
>         > Another (partial) option would be:
>         >
>         > - judgemental equality: written a = b and pronounced “a equals
> b”,
>         > - propositional equality, written Id(a,b) and shortened somehow
> a ? b,
>         > and pronunced ”a idenitfied with b”
>         > (the elements of this type are called “identifications").
>         >
>         > Do either of these seem preferable?
>         > Are there other proposals?
>         > And how should one decide?
>         >
>         > Regards,
>         >
>         > Steve
>         >
>         >
>         >
>         >
>         >
>         > On May 6, 2020, at 12:02 PM, Joyal, André <joyal...@uqam.ca>
> wrote:
>         >
>         > Dear all,
>         >
>         > A few more thoughts.
>         > We all agree that terminology and notation are important.
>         >
>         > I love the story of the equality sign = introduced by Robert
> Recorde (1512-1558).
>         > "because no two things can be more equal than a pair of parallel
> lines".
>         > It took more than a century before been universally adopted.
>         > René Descartes (1596-1650) used a different symbol  in his work
> (something like \alpha).
>         > We may ask why Recorde's notation won over Descartes's notation?
>         > Of course, we may never know.
>         > I dare to say that Recorde's notation was *better*.
>         > Among other things, the equality sign = is symmetric:
>         > the expression a=b and b=a are mirror image of each other.
>         > Recorde's motive for introducing the notation was more about
>         > convenience and aesthetic than about philosophy and history.
>         > The notation was gradually adopted because it is simple and
> useful.
>         > It was not because Recorde was a powerful academic,
>         > since he eventually died in prison.
>         >
>         > There is something to learn from the history of the equality
> sign.
>         > I guess that it can also applied to terminology.
>         > A new notation or terminology has a good chance to be adopted
> universally
>         > if it is simple and useful, but it may take time.
>         >
>         > André
>         > ________________________________
> homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [
> anste...@gmail.com]
>         > Sent: Tuesday, May 05, 2020 4:47 AM
>         > Subject: [HoTT] Identity versus equality
>         >
>         > The discussion yesterday provides a good occasion for me to pose
> a question I have long wanted to put to this list: is there a convention
> generally agreed upon in the HoTT-community for when (if ever) to use
>         >
>         > Here are some relevant data.
>         >
>         > A Germanic equivalent for 'identity' is 'sameness'.
>         > A Germanic equivalent for 'equality' is 'likeness'.
>         >
>         > For Aristotle equality means sameness of quantity. This is how
> one must understand 'equal' in Euclid's Elements, where a triangle may have
> all sides equal (clearly, they cannot be identical). The axiom in the
> Elements that has given rise to the term 'Euclidean relation' and which is
> appealed to in Elements I.1 is phrased in terms of 'equal' rather than
> 'identical'.
>         >
>         > In Diophantus's Arithmetica, on the other hand, the two terms of
> an equation are said to be equal, not identical, and this would become the
> standard terminology in algebra. For instance, the sign '=' was introduced
> by Robert Recorde as a sign of equality, not as a sign of identity. The
> explanation for this apparent discrepancy with the Aristotelian/Euclidean
> terminology might be that when dealing with numbers, equality just is
> identity, since for two numbers to be identical as to magnitude just is for
> them to be the same number. Aristotle says as much in Metaphysics M.7.
>         >
>         > Hilbert and Bernays might be one of the few logic books in the
> modern era to distinguish equality from identity (volume I, chapter 5).
> 'Equality' is there used for any equivalence relation and glossed as the
> obtaining of "irgendeine Art von Übereinstimmung". Identity, by contrast,
> is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility
> within the given language.
>         >
>         > Frege, by contrast, explicitly identifies (sic!) equality with
> identity, and glosses the latter as sameness or coincidence, in the first
> footnote to his paper on sense and reference.  Kleene and Church do the
> same in their famous textbooks: if one looks under 'identity' in the index
> to any of those books one is referred to 'equality'.
>         >
>         > Clearly the two cannot be assumed to mean the same by analysts
> who speak of two functions being identically equal!
>         >
>         > --
>         > 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
> .
>         >
>         > --
>         > 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
> .
>         >
>         >
>         > --
>         > 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
> .
>
>         --
>         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
> .
>
>
>
>
>     This message and any attachment are intended solely for the addressee
>     and may contain confidential information. If you have received this
>     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.
>
>
>
>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> 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
> To view this discussion on the web visit
> .
>

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

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

* Re: [HoTT] Identity versus equality
2020-05-07  6:58            Thorsten Altenkirch
2020-05-07  9:04              Ansten Mørch Klev
@ 2020-05-07 10:09              Thomas Streicher
2020-05-07 16:13                Joyal, André
From: Thomas Streicher @ 2020-05-07 10:09 UTC (permalink / raw)
To: Thorsten Altenkirch
Cc: Joyal, André,

In my eyes the reason for the confusion (or rather different views)
arises from the different situation we have in syntax and in semantics.

In syntax the "real thing" is propositional equality and judgemental
equality is just an auxiliary notion. In mathematics it's the well
known difference between equality requiring proof (e.g. by induction) and
checking equality by mere symbolic computation. The latter is just a
technical device and not something conceptually basic.

The situation is very different in models (be they simplicial, cubical
or whatever). There judgemental equality gets interpreted as equality
of morphism and propositional equality gets interpreted as being homotopic.
Since the outer level of 2-level type theory is extensional there is
no judgemental equality (as in extensional TT).

This latter view is the view of people working in higher dimensional
category theory as e.g. you, Andr'e when you are not posting on the
list but write your beautiful texts on quasicats, Lurie or Cisinski
(and quite a few others). In these works people are not afraid of
refering to equality of objects, e.g. when defining the infinite
dimensional analogue of Grothendieck fibrations. And this for very
good reasons since there are important parts of category theory where
equality of objects does play a role (typically Grothendieck fibrations).

Fibered cats also often don't allow one to speak about equality of
objects in the base but it is there. This is very clearly expressed so
in the last paragraph of B'enabou's JSL article of fibered cats from 1985.
I think this applies equally well to infinity cats mutatis mutandis.

This phenomenon is not new. Consider good old topos theory. There are
things expressible in the internal logic of a topos and there are
things which can't be expressed in it as e.g. well pointedness or
every epi splits. The first holds vacuously when (misleadingly)
expressed in the internal language of a topos and the second amounts
to so called internal AC (which amounts to epis being preserved by
arbitrary exponentiation). This doesn't mean at all that internal language is
a bad thing. It just means that that it has its limitations...

Analogously, so in infinity category theory. Let us assume for a
moment that HoTT were the internal language of infinity toposes (which
I consider as problematic). There are many things which can be
expressed in the internal language but not everything as e.g. being a
Grothendieck fibration or being a mono...

I mean these are facts which one has to accept. One might find them
deplorable or a good thing but one has to accept them...

One of the reasons why I do respect Voevodsky a lot is that although
he developed HoTT (or better the "univalent view") he also suggested
2-level type theory when he saw its limitations.

I hope you apologize but I can't supress the following analogy coming
to my mind. After revolution in Russia and the civil war when economy
lay down the Bolsheviks reintroduced a bit of market economy under the
name NEP (at least that's the acronym in German) to help up the economy.
(To finish the story NEP was abandoned by Stalin which lead to well known
catastrophies like the forced collectivization...)

Sorry for that but one has to be careful when changing things and
think twice before throwing away old things...some of them might be
still useful and even indispensible!

Thomas

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

* RE: [HoTT] Identity versus equality
2020-05-07 10:09              Thomas Streicher
@ 2020-05-07 16:13                Joyal, André
2020-05-07 21:41                  David Roberts
From: Joyal, André @ 2020-05-07 16:13 UTC (permalink / raw)
To: Thomas Streicher, Thorsten Altenkirch
Cc: Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com

Thomas wrote:

<<The situation is very different in models (be they simplicial, cubical
or whatever). There judgemental equality gets interpreted as equality
of morphism and propositional equality gets interpreted as being homotopic.
Since the outer level of 2-level type theory is extensional there is
no judgemental equality (as in extensional TT).>>

I agree, there is some some kind of (weak) Quillen model structure associated to every model of type theory.
All of higher category theory seems to be based on good old set theory.
For example, a quasi-category is a simplicial set.
The category of sets could be replaced by a topos, but a topos is a category
and every category has a set of objects and a set of arrows.
At some level, all mathematics is based on some kind of set theory.
Is it not obvious?
Of course, we could possibly work exclusively with countable sets.
The set of natural numbers is the socle on which all mathematics is constructed.
Still, I would not want to refer constantly to recursion when I do mathematics.
There is a hierarchy of mathematical languages, and Peano's arithmetic is at the ground level.
Modern mathematics is mostly concerned with higher levels of abstraction.
Its usefulness is without questions, athough its foundation can be problematic.
Type theory is the only theory I know which includes two levels in its formalism.
Judgemental equality is at the lower level. It is not inferior, it is more fundamental.

Best,
André

________________________________________
Sent: Thursday, May 07, 2020 6:09 AM
To: Thorsten Altenkirch
Cc: Joyal, André; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

In my eyes the reason for the confusion (or rather different views)
arises from the different situation we have in syntax and in semantics.

In syntax the "real thing" is propositional equality and judgemental
equality is just an auxiliary notion. In mathematics it's the well
known difference between equality requiring proof (e.g. by induction) and
checking equality by mere symbolic computation. The latter is just a
technical device and not something conceptually basic.

The situation is very different in models (be they simplicial, cubical
or whatever). There judgemental equality gets interpreted as equality
of morphism and propositional equality gets interpreted as being homotopic.
Since the outer level of 2-level type theory is extensional there is
no judgemental equality (as in extensional TT).

This latter view is the view of people working in higher dimensional
category theory as e.g. you, Andr'e when you are not posting on the
list but write your beautiful texts on quasicats, Lurie or Cisinski
(and quite a few others). In these works people are not afraid of
refering to equality of objects, e.g. when defining the infinite
dimensional analogue of Grothendieck fibrations. And this for very
good reasons since there are important parts of category theory where
equality of objects does play a role (typically Grothendieck fibrations).

Fibered cats also often don't allow one to speak about equality of
objects in the base but it is there. This is very clearly expressed so
in the last paragraph of B'enabou's JSL article of fibered cats from 1985.
I think this applies equally well to infinity cats mutatis mutandis.

This phenomenon is not new. Consider good old topos theory. There are
things expressible in the internal logic of a topos and there are
things which can't be expressed in it as e.g. well pointedness or
every epi splits. The first holds vacuously when (misleadingly)
expressed in the internal language of a topos and the second amounts
to so called internal AC (which amounts to epis being preserved by
arbitrary exponentiation). This doesn't mean at all that internal language is
a bad thing. It just means that that it has its limitations...

Analogously, so in infinity category theory. Let us assume for a
moment that HoTT were the internal language of infinity toposes (which
I consider as problematic). There are many things which can be
expressed in the internal language but not everything as e.g. being a
Grothendieck fibration or being a mono...

I mean these are facts which one has to accept. One might find them
deplorable or a good thing but one has to accept them...

One of the reasons why I do respect Voevodsky a lot is that although
he developed HoTT (or better the "univalent view") he also suggested
2-level type theory when he saw its limitations.

I hope you apologize but I can't supress the following analogy coming
to my mind. After revolution in Russia and the civil war when economy
lay down the Bolsheviks reintroduced a bit of market economy under the
name NEP (at least that's the acronym in German) to help up the economy.
(To finish the story NEP was abandoned by Stalin which lead to well known
catastrophies like the forced collectivization...)

Sorry for that but one has to be careful when changing things and
think twice before throwing away old things...some of them might be
still useful and even indispensible!

Thomas

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

* Re: [HoTT] Identity versus equality
2020-05-07 16:13                Joyal, André
@ 2020-05-07 21:41                  David Roberts
2020-05-07 23:43                    Joyal, André
From: David Roberts @ 2020-05-07 21:41 UTC (permalink / raw)
To: Joyal, André
Cc: Thomas Streicher, Thorsten Altenkirch, Michael Shulman,

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

>every category has a set of objects and a set of arrows.

I'm sorry, but where does it say that? The whole point of ETCS was to avoid
an ambient set theory, no? Not to mention the original 'General theory of
natural equivalences' avoided defining categories using sets.

Humbly,
David

David Roberts
Webpage: https://ncatlab.org/nlab/show/David+Roberts
Blog: https://thehighergeometer.wordpress.com

On Fri, 8 May 2020 at 01:43, Joyal, André <joyal...@uqam.ca> wrote:

>
> Thomas wrote:
>
> <<The situation is very different in models (be they simplicial, cubical
> or whatever). There judgemental equality gets interpreted as equality
> of morphism and propositional equality gets interpreted as being homotopic.
> Since the outer level of 2-level type theory is extensional there is
> no judgemental equality (as in extensional TT).>>
>
> I agree, there is some some kind of (weak) Quillen model structure
> associated to every model of type theory.
> All of higher category theory seems to be based on good old set theory.
> For example, a quasi-category is a simplicial set.
> The category of sets could be replaced by a topos, but a topos is a
> category
> and every category has a set of objects and a set of arrows.
> At some level, all mathematics is based on some kind of set theory.
> Is it not obvious?
> We cannot escape Kantor's paradise!
> Of course, we could possibly work exclusively with countable sets.
> The set of natural numbers is the socle on which all mathematics is
> constructed.
> Still, I would not want to refer constantly to recursion when I do
> mathematics.
> There is a hierarchy of mathematical languages, and Peano's arithmetic is
> at the ground level.
> Modern mathematics is mostly concerned with higher levels of abstraction.
> Its usefulness is without questions, athough its foundation can be
> problematic.
> Type theory is the only theory I know which includes two levels in its
> formalism.
> Judgemental equality is at the lower level. It is not inferior, it is more
> fundamental.
>
> Best,
> André
>
>
>
> ________________________________________
> Sent: Thursday, May 07, 2020 6:09 AM
> To: Thorsten Altenkirch
> Cc: Joyal, André; Michael Shulman; Steve Awodey;
> Subject: Re: [HoTT] Identity versus equality
>
> In my eyes the reason for the confusion (or rather different views)
> arises from the different situation we have in syntax and in semantics.
>
> In syntax the "real thing" is propositional equality and judgemental
> equality is just an auxiliary notion. In mathematics it's the well
> known difference between equality requiring proof (e.g. by induction) and
> checking equality by mere symbolic computation. The latter is just a
> technical device and not something conceptually basic.
>
> The situation is very different in models (be they simplicial, cubical
> or whatever). There judgemental equality gets interpreted as equality
> of morphism and propositional equality gets interpreted as being homotopic.
> Since the outer level of 2-level type theory is extensional there is
> no judgemental equality (as in extensional TT).
>
> This latter view is the view of people working in higher dimensional
> category theory as e.g. you, Andr'e when you are not posting on the
> list but write your beautiful texts on quasicats, Lurie or Cisinski
> (and quite a few others). In these works people are not afraid of
> refering to equality of objects, e.g. when defining the infinite
> dimensional analogue of Grothendieck fibrations. And this for very
> good reasons since there are important parts of category theory where
> equality of objects does play a role (typically Grothendieck fibrations).
>
> Fibered cats also often don't allow one to speak about equality of
> objects in the base but it is there. This is very clearly expressed so
> in the last paragraph of B'enabou's JSL article of fibered cats from 1985.
> I think this applies equally well to infinity cats mutatis mutandis.
>
> This phenomenon is not new. Consider good old topos theory. There are
> things expressible in the internal logic of a topos and there are
> things which can't be expressed in it as e.g. well pointedness or
> every epi splits. The first holds vacuously when (misleadingly)
> expressed in the internal language of a topos and the second amounts
> to so called internal AC (which amounts to epis being preserved by
> arbitrary exponentiation). This doesn't mean at all that internal language
> is
> a bad thing. It just means that that it has its limitations...
>
> Analogously, so in infinity category theory. Let us assume for a
> moment that HoTT were the internal language of infinity toposes (which
> I consider as problematic). There are many things which can be
> expressed in the internal language but not everything as e.g. being a
> Grothendieck fibration or being a mono...
>
> I mean these are facts which one has to accept. One might find them
> deplorable or a good thing but one has to accept them...
>
> One of the reasons why I do respect Voevodsky a lot is that although
> he developed HoTT (or better the "univalent view") he also suggested
> 2-level type theory when he saw its limitations.
>
> I hope you apologize but I can't supress the following analogy coming
> to my mind. After revolution in Russia and the civil war when economy
> lay down the Bolsheviks reintroduced a bit of market economy under the
> name NEP (at least that's the acronym in German) to help up the economy.
> (To finish the story NEP was abandoned by Stalin which lead to well known
> catastrophies like the forced collectivization...)
>
> Sorry for that but one has to be careful when changing things and
> think twice before throwing away old things...some of them might be
> still useful and even indispensible!
>
> 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
> To view this discussion on the web visit
> .
>

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

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

* RE: [HoTT] Identity versus equality
2020-05-07 21:41                  David Roberts
@ 2020-05-07 23:43                    Joyal, André
2020-05-07 23:56                      David Roberts
From: Joyal, André @ 2020-05-07 23:43 UTC (permalink / raw)
To: David Roberts
Cc: Thomas Streicher, Thorsten Altenkirch, Michael Shulman,

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

Dear David,

This is getting controversial!

As you know, there are many notions of category.
Let me say that an ordinary category with a "set" of objects
and a "set" of arrows lives on the ground floor.
There is then a notion of category internal to a category;
let me say that such categories live on the first floor.
By induction, there a notion of category for every floor.
Of course, one can introduce an abstract notion of category
without specifying the level. For example, one
could consider a type theory classifying the notion of (\infty,1)-category.
But the type theory must be described by specifying a formal system.
The "predicates" in the formal system form a set, actually a countable set.
The syntactic category of any formal system lives on the ground floor.
Hence the generic category lives on the first floor.

I would love to remove set theory (in a naive sense)
from the foundation of mathematics if that were possible.
Is that really desirable?
Maybe we should accept the situation
and use it to improve mathematics.

Best,
André

________________________________
From: David Roberts [drober...@gmail.com]
Sent: Thursday, May 07, 2020 5:41 PM
To: Joyal, André
Cc: Thomas Streicher; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

>every category has a set of objects and a set of arrows.

I'm sorry, but where does it say that? The whole point of ETCS was to avoid an ambient set theory, no? Not to mention the original 'General theory of natural equivalences' avoided defining categories using sets.

Humbly,
David

David Roberts
Webpage: https://ncatlab.org/nlab/show/David+Roberts
Blog: https://thehighergeometer.wordpress.com

On Fri, 8 May 2020 at 01:43, Joyal, André <joyal...@uqam.ca<mailto:joyal...@uqam.ca>> wrote:

Thomas wrote:

<<The situation is very different in models (be they simplicial, cubical
or whatever). There judgemental equality gets interpreted as equality
of morphism and propositional equality gets interpreted as being homotopic.
Since the outer level of 2-level type theory is extensional there is
no judgemental equality (as in extensional TT).>>

I agree, there is some some kind of (weak) Quillen model structure associated to every model of type theory.
All of higher category theory seems to be based on good old set theory.
For example, a quasi-category is a simplicial set.
The category of sets could be replaced by a topos, but a topos is a category
and every category has a set of objects and a set of arrows.
At some level, all mathematics is based on some kind of set theory.
Is it not obvious?
Of course, we could possibly work exclusively with countable sets.
The set of natural numbers is the socle on which all mathematics is constructed.
Still, I would not want to refer constantly to recursion when I do mathematics.
There is a hierarchy of mathematical languages, and Peano's arithmetic is at the ground level.
Modern mathematics is mostly concerned with higher levels of abstraction.
Its usefulness is without questions, athough its foundation can be problematic.
Type theory is the only theory I know which includes two levels in its formalism.
Judgemental equality is at the lower level. It is not inferior, it is more fundamental.

Best,
André

________________________________________
Sent: Thursday, May 07, 2020 6:09 AM
To: Thorsten Altenkirch
Subject: Re: [HoTT] Identity versus equality

In my eyes the reason for the confusion (or rather different views)
arises from the different situation we have in syntax and in semantics.

In syntax the "real thing" is propositional equality and judgemental
equality is just an auxiliary notion. In mathematics it's the well
known difference between equality requiring proof (e.g. by induction) and
checking equality by mere symbolic computation. The latter is just a
technical device and not something conceptually basic.

The situation is very different in models (be they simplicial, cubical
or whatever). There judgemental equality gets interpreted as equality
of morphism and propositional equality gets interpreted as being homotopic.
Since the outer level of 2-level type theory is extensional there is
no judgemental equality (as in extensional TT).

This latter view is the view of people working in higher dimensional
category theory as e.g. you, Andr'e when you are not posting on the
list but write your beautiful texts on quasicats, Lurie or Cisinski
(and quite a few others). In these works people are not afraid of
refering to equality of objects, e.g. when defining the infinite
dimensional analogue of Grothendieck fibrations. And this for very
good reasons since there are important parts of category theory where
equality of objects does play a role (typically Grothendieck fibrations).

Fibered cats also often don't allow one to speak about equality of
objects in the base but it is there. This is very clearly expressed so
in the last paragraph of B'enabou's JSL article of fibered cats from 1985.
I think this applies equally well to infinity cats mutatis mutandis.

This phenomenon is not new. Consider good old topos theory. There are
things expressible in the internal logic of a topos and there are
things which can't be expressed in it as e.g. well pointedness or
every epi splits. The first holds vacuously when (misleadingly)
expressed in the internal language of a topos and the second amounts
to so called internal AC (which amounts to epis being preserved by
arbitrary exponentiation). This doesn't mean at all that internal language is
a bad thing. It just means that that it has its limitations...

Analogously, so in infinity category theory. Let us assume for a
moment that HoTT were the internal language of infinity toposes (which
I consider as problematic). There are many things which can be
expressed in the internal language but not everything as e.g. being a
Grothendieck fibration or being a mono...

I mean these are facts which one has to accept. One might find them
deplorable or a good thing but one has to accept them...

One of the reasons why I do respect Voevodsky a lot is that although
he developed HoTT (or better the "univalent view") he also suggested
2-level type theory when he saw its limitations.

I hope you apologize but I can't supress the following analogy coming
to my mind. After revolution in Russia and the civil war when economy
lay down the Bolsheviks reintroduced a bit of market economy under the
name NEP (at least that's the acronym in German) to help up the economy.
(To finish the story NEP was abandoned by Stalin which lead to well known
catastrophies like the forced collectivization...)

Sorry for that but one has to be careful when changing things and
think twice before throwing away old things...some of them might be
still useful and even indispensible!

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

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

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

* Re: [HoTT] Identity versus equality
2020-05-07 23:43                    Joyal, André
@ 2020-05-07 23:56                      David Roberts
2020-05-08  6:40                        Thomas Streicher
From: David Roberts @ 2020-05-07 23:56 UTC (permalink / raw)
To: Joyal, André
Cc: Thomas Streicher, Thorsten Altenkirch, Michael Shulman,

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

Dear André,

I merely meant that the definition of category only requires first-order
logic as in (Eilenberg–Mac Lane 1945), or at best a low-level dependent
type theory (
https://ncatlab.org/nlab/show/type-theoretic+definition+of+category). See
also: https://ncatlab.org/nlab/show/fully+formal+ETCS#the_theory_etcs

Regards,
David

David Roberts
Webpage: https://ncatlab.org/nlab/show/David+Roberts
Blog: https://thehighergeometer.wordpress.com

On Fri, 8 May 2020 at 09:13, Joyal, André <joyal...@uqam.ca> wrote:

> Dear David,
>
> This is getting controversial!
>
> As you know, there are many notions of category.
> Let me say that an ordinary category with a "set" of objects
> and a "set" of arrows lives on the ground floor.
> There is then a notion of category internal to a category;
> let me say that such categories live on the first floor.
> By induction, there a notion of category for every floor.
> Of course, one can introduce an abstract notion of category
> without specifying the level. For example, one
> could consider a type theory classifying the notion of (\infty,1)-category.
> But the type theory must be described by specifying a formal system.
> The "predicates" in the formal system form a set, actually a countable set.
> The syntactic category of any formal system lives on the ground floor.
> Hence the generic category lives on the first floor.
>
> I would love to remove set theory (in a naive sense)
> from the foundation of mathematics if that were possible.
> Is that really desirable?
> Maybe we should accept the situation
> and use it to improve mathematics.
>
> Best,
> André
>
> ------------------------------
> *From:* David Roberts [drober...@gmail.com]
> *Sent:* Thursday, May 07, 2020 5:41 PM
> *To:* Joyal, André
> *Cc:* Thomas Streicher; Thorsten Altenkirch; Michael Shulman; Steve
> *Subject:* Re: [HoTT] Identity versus equality
>
> >every category has a set of objects and a set of arrows.
>
> I'm sorry, but where does it say that? The whole point of ETCS was to
> avoid an ambient set theory, no? Not to mention the original 'General
> theory of natural equivalences' avoided defining categories using sets.
>
> Humbly,
> David
>
>
> David Roberts
> Webpage: https://ncatlab.org/nlab/show/David+Roberts
> Blog: https://thehighergeometer.wordpress.com
>
>
> On Fri, 8 May 2020 at 01:43, Joyal, André <joyal...@uqam.ca> wrote:
>
>>
>> Thomas wrote:
>>
>> <<The situation is very different in models (be they simplicial, cubical
>> or whatever). There judgemental equality gets interpreted as equality
>> of morphism and propositional equality gets interpreted as being
>> homotopic.
>> Since the outer level of 2-level type theory is extensional there is
>> no judgemental equality (as in extensional TT).>>
>>
>> I agree, there is some some kind of (weak) Quillen model structure
>> associated to every model of type theory.
>> All of higher category theory seems to be based on good old set theory.
>> For example, a quasi-category is a simplicial set.
>> The category of sets could be replaced by a topos, but a topos is a
>> category
>> and every category has a set of objects and a set of arrows.
>> At some level, all mathematics is based on some kind of set theory.
>> Is it not obvious?
>> We cannot escape Kantor's paradise!
>> Of course, we could possibly work exclusively with countable sets.
>> The set of natural numbers is the socle on which all mathematics is
>> constructed.
>> Still, I would not want to refer constantly to recursion when I do
>> mathematics.
>> There is a hierarchy of mathematical languages, and Peano's arithmetic is
>> at the ground level.
>> Modern mathematics is mostly concerned with higher levels of abstraction.
>> Its usefulness is without questions, athough its foundation can be
>> problematic.
>> Type theory is the only theory I know which includes two levels in its
>> formalism.
>> Judgemental equality is at the lower level. It is not inferior, it is
>> more fundamental.
>>
>> Best,
>> André
>>
>>
>>
>> ________________________________________
>> Sent: Thursday, May 07, 2020 6:09 AM
>> To: Thorsten Altenkirch
>> Cc: Joyal, André; Michael Shulman; Steve Awodey;
>> Subject: Re: [HoTT] Identity versus equality
>>
>> In my eyes the reason for the confusion (or rather different views)
>> arises from the different situation we have in syntax and in semantics.
>>
>> In syntax the "real thing" is propositional equality and judgemental
>> equality is just an auxiliary notion. In mathematics it's the well
>> known difference between equality requiring proof (e.g. by induction) and
>> checking equality by mere symbolic computation. The latter is just a
>> technical device and not something conceptually basic.
>>
>> The situation is very different in models (be they simplicial, cubical
>> or whatever). There judgemental equality gets interpreted as equality
>> of morphism and propositional equality gets interpreted as being
>> homotopic.
>> Since the outer level of 2-level type theory is extensional there is
>> no judgemental equality (as in extensional TT).
>>
>> This latter view is the view of people working in higher dimensional
>> category theory as e.g. you, Andr'e when you are not posting on the
>> list but write your beautiful texts on quasicats, Lurie or Cisinski
>> (and quite a few others). In these works people are not afraid of
>> refering to equality of objects, e.g. when defining the infinite
>> dimensional analogue of Grothendieck fibrations. And this for very
>> good reasons since there are important parts of category theory where
>> equality of objects does play a role (typically Grothendieck fibrations).
>>
>> Fibered cats also often don't allow one to speak about equality of
>> objects in the base but it is there. This is very clearly expressed so
>> in the last paragraph of B'enabou's JSL article of fibered cats from 1985.
>> I think this applies equally well to infinity cats mutatis mutandis.
>>
>> This phenomenon is not new. Consider good old topos theory. There are
>> things expressible in the internal logic of a topos and there are
>> things which can't be expressed in it as e.g. well pointedness or
>> every epi splits. The first holds vacuously when (misleadingly)
>> expressed in the internal language of a topos and the second amounts
>> to so called internal AC (which amounts to epis being preserved by
>> arbitrary exponentiation). This doesn't mean at all that internal
>> language is
>> a bad thing. It just means that that it has its limitations...
>>
>> Analogously, so in infinity category theory. Let us assume for a
>> moment that HoTT were the internal language of infinity toposes (which
>> I consider as problematic). There are many things which can be
>> expressed in the internal language but not everything as e.g. being a
>> Grothendieck fibration or being a mono...
>>
>> I mean these are facts which one has to accept. One might find them
>> deplorable or a good thing but one has to accept them...
>>
>> One of the reasons why I do respect Voevodsky a lot is that although
>> he developed HoTT (or better the "univalent view") he also suggested
>> 2-level type theory when he saw its limitations.
>>
>> I hope you apologize but I can't supress the following analogy coming
>> to my mind. After revolution in Russia and the civil war when economy
>> lay down the Bolsheviks reintroduced a bit of market economy under the
>> name NEP (at least that's the acronym in German) to help up the economy.
>> (To finish the story NEP was abandoned by Stalin which lead to well known
>> catastrophies like the forced collectivization...)
>>
>> Sorry for that but one has to be careful when changing things and
>> think twice before throwing away old things...some of them might be
>> still useful and even indispensible!
>>
>> 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
>> To view this discussion on the web visit
>> .
>>
>

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

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

* Re: [HoTT] Identity versus equality
2020-05-07 23:56                      David Roberts
@ 2020-05-08  6:40                        Thomas Streicher
2020-05-08 21:06                          Joyal, André
From: Thomas Streicher @ 2020-05-08  6:40 UTC (permalink / raw)
To: David Roberts
Cc: Joyal, André,
Thorsten Altenkirch, Michael Shulman, Steve Awodey,

Dear Robert,

in what I said I didn't mean set theory literally. I was rather referring
to all kinds of categorical logic where equality is interpreted as
(fiberwise) diagonal like (traditional) topos theory in particular.
These kinds of gadgets all have the advantage that "Set" is not ruled
out as a model.

Since the diagonal is hardly ever fibrant HoTT rules out Set as a model.

But this is not my main problem. My main problem is that there is at least
one area of category theory where one has to speak about equality of
objects and these are Grothendieck fibrations. And these are intrinsic
for doing topos theory over general base toposes.
(That I really like them is, admittedly, also an important reason for me
not being ready to give them up! And for reasons of personal and
cultural "antagonisms" they are not very popular among the majority of
category theorists... Thus, there are many people who would not be too
But I want to emphasize that real masters of infinite dimensional
categories do not have the faintest problem speaking about equality
when speaking about infinite dimensional versions of Grothendieck
fibrations!)

Though (traditional) topos theory can be developed over fairly general
toposes and this, at least philosophically, is an important aspect one
cannot deny that most toposes of interest heavily rely on Set, be they
of the Grothendieck kind or be they of the realizability kind!

Thomas

PS  Above I put Set into inverted commas because the logician in me
finds it amusing to speak about "the" category of sets which is
nothing but an illusion... Even the nowadays not so little number of
But even the "universe" view is nothing but an ideology because since
Cohen set theory is mainly a business of constructing different models
via forcing.
Thus, since Set is (sort of) an illusion it is important to do toposes
over arbitrary bases for which purpose one needs Grothendieck fibrations
which do not make sense without equality of objects.

PPS Some people might get the impression I am a "crypto set
theorist". Nothing could be more wrong. I am anti-ideological and
pluralist and I like "deviating" ideas. But I am interested in
calibrating what one needs for which goals. What I am allergic at is
ideological positions which want to forbid someone doing certain
things because they do not fit to some ideological positions...
And one has to accept that not all combinations are possible. Thus
pluralist is better to inegrist!

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

* RE: [HoTT] Identity versus equality
2020-05-08  6:40                        Thomas Streicher
@ 2020-05-08 21:06                          Joyal, André
2020-05-08 23:44                            Steve Awodey
2020-05-09  8:28                            Thomas Streicher
0 siblings, 2 replies; 61+ messages in thread
From: Joyal, André @ 2020-05-08 21:06 UTC (permalink / raw)
To: Thomas Streicher, David Roberts
Cc: Thorsten Altenkirch, Michael Shulman, Steve Awodey,

Dear Thomas,

You are right, the equality of objects in a Grothendieck fibration is judgemental.

Propositional equality of type theory has been studied a lot during the last decades.
I feel quite confortable with it, with the homotopy interpretation and the univalence principle, etc.
I confess that I am much less at ease with judgmental equality and the syntax of type theory.
Until now, type theory has failed to prove that pi_4(S^3)=C_2.
Is it the symptom of a fundamental problem?
Is it because the reduction algoritms are not optimal?
Or because computers are not powerful enough?
What is the abstract theory of terms reduction in type theory?
I apologise for my ignorance.

Best,
André

________________________________________t
Sent: Friday, May 08, 2020 2:40 AM
To: David Roberts
Cc: Joyal, André; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

Dear Robert,

in what I said I didn't mean set theory literally. I was rather referring
to all kinds of categorical logic where equality is interpreted as
(fiberwise) diagonal like (traditional) topos theory in particular.
These kinds of gadgets all have the advantage that "Set" is not ruled
out as a model.

Since the diagonal is hardly ever fibrant HoTT rules out Set as a model.

But this is not my main problem. My main problem is that there is at least
one area of category theory where one has to speak about equality of
objects and these are Grothendieck fibrations. And these are intrinsic
for doing topos theory over general base toposes.
(That I really like them is, admittedly, also an important reason for me
not being ready to give them up! And for reasons of personal and
cultural "antagonisms" they are not very popular among the majority of
category theorists... Thus, there are many people who would not be too
But I want to emphasize that real masters of infinite dimensional
categories do not have the faintest problem speaking about equality
when speaking about infinite dimensional versions of Grothendieck
fibrations!)

Though (traditional) topos theory can be developed over fairly general
toposes and this, at least philosophically, is an important aspect one
cannot deny that most toposes of interest heavily rely on Set, be they
of the Grothendieck kind or be they of the realizability kind!

Thomas

PS  Above I put Set into inverted commas because the logician in me
finds it amusing to speak about "the" category of sets which is
nothing but an illusion... Even the nowadays not so little number of
But even the "universe" view is nothing but an ideology because since
Cohen set theory is mainly a business of constructing different models
via forcing.
Thus, since Set is (sort of) an illusion it is important to do toposes
over arbitrary bases for which purpose one needs Grothendieck fibrations
which do not make sense without equality of objects.

PPS Some people might get the impression I am a "crypto set
theorist". Nothing could be more wrong. I am anti-ideological and
pluralist and I like "deviating" ideas. But I am interested in
calibrating what one needs for which goals. What I am allergic at is
ideological positions which want to forbid someone doing certain
things because they do not fit to some ideological positions...
And one has to accept that not all combinations are possible. Thus
pluralist is better to inegrist!

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

* Re: [HoTT] Identity versus equality
2020-05-08 21:06                          Joyal, André
@ 2020-05-08 23:44                            Steve Awodey
2020-05-09  2:46                              Joyal, André
2020-05-09  8:28                            Thomas Streicher
1 sibling, 2 replies; 61+ messages in thread
From: Steve Awodey @ 2020-05-08 23:44 UTC (permalink / raw)
To:  Joyal, André
Cc: Thomas Streicher, David Roberts, Thorsten Altenkirch,

Dear André,

I would prefer to say that t current systems of type theory have failed to *compute* pi_4(S^3), so as not to diminish the value of Guillaume’s beautiful proof, which has even been formally checked in different proof assistants.
You of course know the difference between proving something in type theory and computing the value of a term, but some readers may not.

Best wishes,

Steve

Ps: In my opinion, for what it’s worth, making a system that will compute the value of Brunerie’s constant is an engineering problem, not a mathematical one. Which is not to say it would not be an important advance!

> On May 8, 2020, at 17:06, Joyal, André <joyal...@uqam.ca> wrote:
>
> ﻿Dear Thomas,
>
> You are right, the equality of objects in a Grothendieck fibration is judgemental.
>
> Propositional equality of type theory has been studied a lot during the last decades.
> I feel quite confortable with it, with the homotopy interpretation and the univalence principle, etc.
> I confess that I am much less at ease with judgmental equality and the syntax of type theory.
> Until now, type theory has failed to prove that pi_4(S^3)=C_2.
> Is it the symptom of a fundamental problem?
> Is it because the reduction algoritms are not optimal?
> Or because computers are not powerful enough?
> What is the abstract theory of terms reduction in type theory?
> I apologise for my ignorance.
>
> Best,
> André
>
> ________________________________________t
> Sent: Friday, May 08, 2020 2:40 AM
> To: David Roberts
> Cc: Joyal, André; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
> Subject: Re: [HoTT] Identity versus equality
>
> Dear Robert,
>
> in what I said I didn't mean set theory literally. I was rather referring
> to all kinds of categorical logic where equality is interpreted as
> (fiberwise) diagonal like (traditional) topos theory in particular.
> These kinds of gadgets all have the advantage that "Set" is not ruled
> out as a model.
>
> Since the diagonal is hardly ever fibrant HoTT rules out Set as a model.
>
> But this is not my main problem. My main problem is that there is at least
> one area of category theory where one has to speak about equality of
> objects and these are Grothendieck fibrations. And these are intrinsic
> for doing topos theory over general base toposes.
> (That I really like them is, admittedly, also an important reason for me
> not being ready to give them up! And for reasons of personal and
> cultural "antagonisms" they are not very popular among the majority of
> category theorists... Thus, there are many people who would not be too
> But I want to emphasize that real masters of infinite dimensional
> categories do not have the faintest problem speaking about equality
> when speaking about infinite dimensional versions of Grothendieck
> fibrations!)
>
> Though (traditional) topos theory can be developed over fairly general
> toposes and this, at least philosophically, is an important aspect one
> cannot deny that most toposes of interest heavily rely on Set, be they
> of the Grothendieck kind or be they of the realizability kind!
>
> Thomas
>
> PS  Above I put Set into inverted commas because the logician in me
> finds it amusing to speak about "the" category of sets which is
> nothing but an illusion... Even the nowadays not so little number of
> But even the "universe" view is nothing but an ideology because since
> Cohen set theory is mainly a business of constructing different models
> via forcing.
> Thus, since Set is (sort of) an illusion it is important to do toposes
> over arbitrary bases for which purpose one needs Grothendieck fibrations
> which do not make sense without equality of objects.
>
> PPS Some people might get the impression I am a "crypto set
> theorist". Nothing could be more wrong. I am anti-ideological and
> pluralist and I like "deviating" ideas. But I am interested in
> calibrating what one needs for which goals. What I am allergic at is
> ideological positions which want to forbid someone doing certain
> things because they do not fit to some ideological positions...
> And one has to accept that not all combinations are possible. Thus
> pluralist is better to inegrist!
>
> --
> 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/8C57894C7413F04A98DDF5629FEC90B1652F54CC%40Pli.gst.uqam.ca.

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

* RE: [HoTT] Identity versus equality
2020-05-08 23:44                            Steve Awodey
@ 2020-05-09  2:46                              Joyal, André
2020-05-09  3:09                                Jon Sterling
[not found]                              <CADZEZBY+3z6nrRwsx9p-HqYuTxAnwMUHv7JasHy8aoy1oaGPcw@mail.gmail.com>
From: Joyal, André @ 2020-05-09  2:46 UTC (permalink / raw)
To: Steve Awodey
Cc: Thomas Streicher, David Roberts, Thorsten Altenkirch,

Dear Steve,

Thank you for stressing the distinction between computing and proving.
I was thinking about the computation of a natural number by reduction of terms.
I must be confused.

But in type theory, is it not true that every proof is a computation?

Best,
André

________________________________________
From: Steve Awodey [steve...@gmail.com]
Sent: Friday, May 08, 2020 7:44 PM
To: Joyal, André
Cc: Thomas Streicher; David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

Dear André,

I would prefer to say that t current systems of type theory have failed to *compute* pi_4(S^3), so as not to diminish the value of Guillaume’s beautiful proof, which has even been formally checked in different proof assistants.
You of course know the difference between proving something in type theory and computing the value of a term, but some readers may not.

Best wishes,

Steve

Ps: In my opinion, for what it’s worth, making a system that will compute the value of Brunerie’s constant is an engineering problem, not a mathematical one. Which is not to say it would not be an important advance!

> On May 8, 2020, at 17:06, Joyal, André <joyal...@uqam.ca> wrote:
>
> ﻿Dear Thomas,
>
> You are right, the equality of objects in a Grothendieck fibration is judgemental.
>
> Propositional equality of type theory has been studied a lot during the last decades.
> I feel quite confortable with it, with the homotopy interpretation and the univalence principle, etc.
> I confess that I am much less at ease with judgmental equality and the syntax of type theory.
> Until now, type theory has failed to prove that pi_4(S^3)=C_2.
> Is it the symptom of a fundamental problem?
> Is it because the reduction algoritms are not optimal?
> Or because computers are not powerful enough?
> What is the abstract theory of terms reduction in type theory?
> I apologise for my ignorance.
>
> Best,
> André
>
> ________________________________________t
> Sent: Friday, May 08, 2020 2:40 AM
> To: David Roberts
> Cc: Joyal, André; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
> Subject: Re: [HoTT] Identity versus equality
>
> Dear Robert,
>
> in what I said I didn't mean set theory literally. I was rather referring
> to all kinds of categorical logic where equality is interpreted as
> (fiberwise) diagonal like (traditional) topos theory in particular.
> These kinds of gadgets all have the advantage that "Set" is not ruled
> out as a model.
>
> Since the diagonal is hardly ever fibrant HoTT rules out Set as a model.
>
> But this is not my main problem. My main problem is that there is at least
> one area of category theory where one has to speak about equality of
> objects and these are Grothendieck fibrations. And these are intrinsic
> for doing topos theory over general base toposes.
> (That I really like them is, admittedly, also an important reason for me
> not being ready to give them up! And for reasons of personal and
> cultural "antagonisms" they are not very popular among the majority of
> category theorists... Thus, there are many people who would not be too
> But I want to emphasize that real masters of infinite dimensional
> categories do not have the faintest problem speaking about equality
> when speaking about infinite dimensional versions of Grothendieck
> fibrations!)
>
> Though (traditional) topos theory can be developed over fairly general
> toposes and this, at least philosophically, is an important aspect one
> cannot deny that most toposes of interest heavily rely on Set, be they
> of the Grothendieck kind or be they of the realizability kind!
>
> Thomas
>
> PS  Above I put Set into inverted commas because the logician in me
> finds it amusing to speak about "the" category of sets which is
> nothing but an illusion... Even the nowadays not so little number of
> But even the "universe" view is nothing but an ideology because since
> Cohen set theory is mainly a business of constructing different models
> via forcing.
> Thus, since Set is (sort of) an illusion it is important to do toposes
> over arbitrary bases for which purpose one needs Grothendieck fibrations
> which do not make sense without equality of objects.
>
> PPS Some people might get the impression I am a "crypto set
> theorist". Nothing could be more wrong. I am anti-ideological and
> pluralist and I like "deviating" ideas. But I am interested in
> calibrating what one needs for which goals. What I am allergic at is
> ideological positions which want to forbid someone doing certain
> things because they do not fit to some ideological positions...
> And one has to accept that not all combinations are possible. Thus
> pluralist is better to inegrist!
>
> --
> 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/8C57894C7413F04A98DDF5629FEC90B1652F54CC%40Pli.gst.uqam.ca.

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

* Re: [HoTT] Identity versus equality
@ 2020-05-09  2:50                                Steve Awodey
0 siblings, 0 replies; 61+ messages in thread
From: Steve Awodey @ 2020-05-09  2:50 UTC (permalink / raw)
To: Homotopy Type Theory; +Cc: "Joyal, André"

To elaborate a bit further in response to some private inquiries:

Brunerie’s proof that pi_4(S^3) = Z_2 , which is an entirely formal proof within homotopy type theory, has two main parts:

(1) it is shown that there is a natural number n such that pi_4(S^3) = Z_n ,
(2) it is shown that n = 2.

Since the proof of (1) is constructive, it produces an actual term t : Nat .
In a system of type theory with the canonicity property
(like intensional MLTT w/o HITs or UA, or some of the more recent cubical type theories),
there is an algorithm which, from any such term t : Nat, will *compute* a numeral t* such that t* == t (definitionally).
This numeral t* denotes a natural number directly.

Applying the algorithm to (the term representing) “Brunerie’s number” n in (1),
we should be able to use it to *compute* that n = 2, avoiding the need for the (quite intricate) proof in part (2).
This is the part that (up to now) has not been possible to do *in practice*, as Andre’ Joyal was pointing out.
Thus we still require the proof in (2) to know that n = 2.

The system of “Book HoTT” allows to formally prove many things that cannot be computed in that system,
because terms coming from HITs or involving UA need not compute.
An advantage of cubical systems is that all terms compute — in principle.
But more practical work seems to be required in order to take advantage of this feature in practice.

Regards,

Steve

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

* Re: [HoTT] Identity versus equality
2020-05-09  2:46                              Joyal, André
@ 2020-05-09  3:09                                Jon Sterling
0 siblings, 0 replies; 61+ messages in thread
From: Jon Sterling @ 2020-05-09  3:09 UTC (permalink / raw)
To: 'Martin Escardo' via Homotopy Type Theory

Dear André,

To answer your question about what is the abstract theory of term reduction in type theory, one very beautiful option is rewriting theory, the study of abstract rewriting systems; this is perhaps the most venerable and mathematically deep tool to study term reduction, but it does not readily support many of the kinds of "reductions" that occur in dependent type theory, especially the more exotic cubical type theories.

For this and other reasons, some of us (including Steve and myself and many others) have been lately studying computation in these type theories using more abstract tools like Artin gluing --- the disadvantage of this approach is the gluing has little to say about the efficiency or algorithmic aspects of computation in type theory, but it is enough to prove that existence proofs do carry algorithms to compute numerals.

Simultaneously, we are working on improving the algorithmic / practical aspects of cubical type theory so that in the future we may be able to actually execute the algorithm that corresponds to Brunerie's proof. My collaborators and I are currently experimentally programming a new reduction algorithm for cubical type theory that I designed this fall; I do not know whether it will help significantly, but we will see.

Best,
Jon

On Fri, May 8, 2020, at 10:46 PM, Joyal, André wrote:
> Dear Steve,
>
> Thank you for stressing the distinction between computing and proving.
> I was thinking about the computation of a natural number by reduction of terms.
> I must be confused.
>
> But in type theory, is it not true that every proof is a computation?
>
> Best,
> André
>
>
>
>
>
> ________________________________________
> From: Steve Awodey [steve...@gmail.com]
> Sent: Friday, May 08, 2020 7:44 PM
> To: Joyal, André
> Cc: Thomas Streicher; David Roberts; Thorsten Altenkirch; Michael
> Subject: Re: [HoTT] Identity versus equality
>
> Dear André,
>
> I would prefer to say that t current systems of type theory have failed
> to *compute* pi_4(S^3), so as not to diminish the value of Guillaume’s
> beautiful proof, which has even been formally checked in different
> proof assistants.
> You of course know the difference between proving something in type
> theory and computing the value of a term, but some readers may not.
>
> Best wishes,
>
> Steve
>
> Ps: In my opinion, for what it’s worth, making a system that will
> compute the value of Brunerie’s constant is an engineering problem, not
> a mathematical one. Which is not to say it would not be an important
>
> > On May 8, 2020, at 17:06, Joyal, André <joyal...@uqam.ca> wrote:
> >
> > ﻿Dear Thomas,
> >
> > You are right, the equality of objects in a Grothendieck fibration is judgemental.
> >
> > Propositional equality of type theory has been studied a lot during the last decades.
> > I feel quite confortable with it, with the homotopy interpretation and the univalence principle, etc.
> > I confess that I am much less at ease with judgmental equality and the syntax of type theory.
> > Until now, type theory has failed to prove that pi_4(S^3)=C_2.
> > Is it the symptom of a fundamental problem?
> > Is it because the reduction algoritms are not optimal?
> > Or because computers are not powerful enough?
> > What is the abstract theory of terms reduction in type theory?
> > I apologise for my ignorance.
> >
> > Best,
> > André
> >
> > ________________________________________t
> > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
> > Sent: Friday, May 08, 2020 2:40 AM
> > To: David Roberts
> > Cc: Joyal, André; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
> > Subject: Re: [HoTT] Identity versus equality
> >
> > Dear Robert,
> >
> > in what I said I didn't mean set theory literally. I was rather referring
> > to all kinds of categorical logic where equality is interpreted as
> > (fiberwise) diagonal like (traditional) topos theory in particular.
> > These kinds of gadgets all have the advantage that "Set" is not ruled
> > out as a model.
> >
> > Since the diagonal is hardly ever fibrant HoTT rules out Set as a model.
> >
> > But this is not my main problem. My main problem is that there is at least
> > one area of category theory where one has to speak about equality of
> > objects and these are Grothendieck fibrations. And these are intrinsic
> > for doing topos theory over general base toposes.
> > (That I really like them is, admittedly, also an important reason for me
> > not being ready to give them up! And for reasons of personal and
> > cultural "antagonisms" they are not very popular among the majority of
> > category theorists... Thus, there are many people who would not be too
> > But I want to emphasize that real masters of infinite dimensional
> > categories do not have the faintest problem speaking about equality
> > when speaking about infinite dimensional versions of Grothendieck
> > fibrations!)
> >
> > Though (traditional) topos theory can be developed over fairly general
> > toposes and this, at least philosophically, is an important aspect one
> > cannot deny that most toposes of interest heavily rely on Set, be they
> > of the Grothendieck kind or be they of the realizability kind!
> >
> > Thomas
> >
> > PS  Above I put Set into inverted commas because the logician in me
> > finds it amusing to speak about "the" category of sets which is
> > nothing but an illusion... Even the nowadays not so little number of
> > But even the "universe" view is nothing but an ideology because since
> > Cohen set theory is mainly a business of constructing different models
> > via forcing.
> > Thus, since Set is (sort of) an illusion it is important to do toposes
> > over arbitrary bases for which purpose one needs Grothendieck fibrations
> > which do not make sense without equality of objects.
> >
> > PPS Some people might get the impression I am a "crypto set
> > theorist". Nothing could be more wrong. I am anti-ideological and
> > pluralist and I like "deviating" ideas. But I am interested in
> > calibrating what one needs for which goals. What I am allergic at is
> > ideological positions which want to forbid someone doing certain
> > things because they do not fit to some ideological positions...
> > And one has to accept that not all combinations are possible. Thus
> > pluralist is better to inegrist!
> >
> > --
> > 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/8C57894C7413F04A98DDF5629FEC90B1652F54CC%40Pli.gst.uqam.ca.
>
> --
> 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
> To view this discussion on the web visit
>

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

* Re: [HoTT] Identity versus equality
2020-05-08 21:06                          Joyal, André
2020-05-08 23:44                            Steve Awodey
@ 2020-05-09  8:28                            Thomas Streicher
2020-05-09 15:53                              Joyal, André
From: Thomas Streicher @ 2020-05-09  8:28 UTC (permalink / raw)
To: Joyal, André
Cc: David Roberts, Thorsten Altenkirch, Michael Shulman,

Dear Andr'e,

in most models of HoTT judgemental equality is equality of morphisms
and propositional equality is being homotopic.
But that is very different from its appearance in formal systems
where judgemental equality is much more restricted and just serves the
purpose of computation. There are artificial versions of type theory
with excessively few computation rules (only mere lambda calculus).

I fully understand why you find judgemental equality puzzling: it is
of very subjective nature. Mathematicians are typically interested in
equalities which are not decided by a rewrite system.
Judgemental equality has a very subjective nature because it
identifies a computational fragment of mathematics and there are many
different such. In Book HoTT one is as computational as traditional
intensional TT is and then adds univalence which lacks any
computational meaning. This is at least frivolous from the perspective
of a traditionalist type theorist... But it is ok and was implemented
in the NuPrl system.

Now for people who use type theory as a way of doing homotopy theory
synthetically the computational aspect is absolutely irrelevant a
priori. When one does ordinary math (including homotopy) computability
is a gimmick and no one would insist on everything being computable.

So if one has shown that the homotopy group of some pointed space is
Z_n for some n and one wants to know what n is then in Book HoTT you
have to guess n and then show that n equal your guess. In cubical type
theory in principle the n can be computed but it may take a very long
time (or the normalization proof is faulty :-)).

The main problem is that programs extracted from proofs are typically
not very efficient (well in rare cases they are but you have to be lucky).

Anyway, my brief answer to the question you raise is:
(1) conceptually judgemental equality is absolutely redundant
and hopelessly subjective
(2) systems with a bare minimum of judgemental equality are not
suitable for the various proof checkers in use since then every
computation has to be done by hand.

Thomas

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

* RE: [HoTT] Identity versus equality
2020-05-09  8:28                            Thomas Streicher
@ 2020-05-09 15:53                              Joyal, André
2020-05-09 18:43                                Thomas Streicher
From: Joyal, André @ 2020-05-09 15:53 UTC (permalink / raw)
To: Thomas Streicher
Cc: David Roberts, Thorsten Altenkirch, Michael Shulman,

Thank you Thomas, Jon and Steve for answering my question.

You are very generous to an old man.
Let me pretend that I still have enough time to study the computational aspects of type theory.

By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
The dream of a formal system in which every proof leads to an actual computation may be far off.
Not that we should abandon it, new discoveries are always possible.
Is there a version of type theory for proving and verifying, less for computing?
The notations of type theory are very useful in homotopy theory.
But the absence of simplicial types is a serious obstacle to applications.

Best,
André

________________________________________
Sent: Saturday, May 09, 2020 4:28 AM
To: Joyal, André
Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

Dear Andr'e,

in most models of HoTT judgemental equality is equality of morphisms
and propositional equality is being homotopic.
But that is very different from its appearance in formal systems
where judgemental equality is much more restricted and just serves the
purpose of computation. There are artificial versions of type theory
with excessively few computation rules (only mere lambda calculus).

I fully understand why you find judgemental equality puzzling: it is
of very subjective nature. Mathematicians are typically interested in
equalities which are not decided by a rewrite system.
Judgemental equality has a very subjective nature because it
identifies a computational fragment of mathematics and there are many
different such. In Book HoTT one is as computational as traditional
intensional TT is and then adds univalence which lacks any
computational meaning. This is at least frivolous from the perspective
of a traditionalist type theorist... But it is ok and was implemented
in the NuPrl system.

Now for people who use type theory as a way of doing homotopy theory
synthetically the computational aspect is absolutely irrelevant a
priori. When one does ordinary math (including homotopy) computability
is a gimmick and no one would insist on everything being computable.

So if one has shown that the homotopy group of some pointed space is
Z_n for some n and one wants to know what n is then in Book HoTT you
have to guess n and then show that n equal your guess. In cubical type
theory in principle the n can be computed but it may take a very long
time (or the normalization proof is faulty :-)).

The main problem is that programs extracted from proofs are typically
not very efficient (well in rare cases they are but you have to be lucky).

Anyway, my brief answer to the question you raise is:
(1) conceptually judgemental equality is absolutely redundant
and hopelessly subjective
(2) systems with a bare minimum of judgemental equality are not
suitable for the various proof checkers in use since then every
computation has to be done by hand.

Thomas

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

* Re: [HoTT] Identity versus equality
2020-05-09 15:53                              Joyal, André
@ 2020-05-09 18:43                                Thomas Streicher
2020-05-09 20:18                                  Joyal, André
From: Thomas Streicher @ 2020-05-09 18:43 UTC (permalink / raw)
To: Joyal, André
Cc: David Roberts, Thorsten Altenkirch, Michael Shulman,

Dear Andr'e,

> By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
> The dream of a formal system in which every proof leads to an actual computation may be far off.
> Not that we should abandon it, new discoveries are always possible.
> Is there a version of type theory for proving and verifying, less
> for computing?

In my opinion the currenrly implemented type theories are essentially
for proving and not for computing.
But if you haven't mechanized PART of equational reasoning it would be
much much more painful than it still is.
But that is "only" a pragmatic issue.

> The notations of type theory are very useful in homotopy theory.
> But the absence of simplicial types is a serious obstacle to applications.

In cubical type theory they sort of live well with cubes not being
fibrant... They have them as pretypes. But maybe I misunderstand...

Thomas

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

* RE: [HoTT] Identity versus equality
2020-05-09 18:43                                Thomas Streicher
@ 2020-05-09 20:18                                  Joyal, André
2020-05-09 21:27                                    Jon Sterling
 (2 more replies)
0 siblings, 3 replies; 61+ messages in thread
From: Joyal, André @ 2020-05-09 20:18 UTC (permalink / raw)
To: Thomas Streicher
Cc: David Roberts, Thorsten Altenkirch, Michael Shulman,

Dear Thomas,

You wrote

<<In my opinion the currenrly implemented type theories are essentially
for proving and not for computing.
But if you haven't mechanized PART of equational reasoning it would be
much much more painful than it still is.
But that is "only" a pragmatic issue.>>

Type  theory has very nice features. I wish they could be preserved and developped further.
But I find it frustrating that I cant do my everyday mathematics with it.
For example, I cannot  say

(1) Let X:\Delta^{op}---->Type be a simplicial type;
(2) Let G be a type equipped with a group structure;
(3) Let BG be the classifying space of a group G;
(4) Let Gr be the category of groups;
(5) Let SType be the category of simplical types.
(6) Let Map(X,Y) be the simplicial types of maps X--->Y
between two simplicial types X and Y.

It is crucial to have (1)
For example, a group could be defined to
be a simplicial object satisfying the Segal conditions.
The classifying space of a group is the colimit of this simplicial object.
The category of groups can be defined to be
a simplicial objects satisfiying the Rezk conditions (a complete Segal space).

Is there some aspects of type theory that we may give up as a price
for solving these problems ?

Best,
André

________________________________________
Sent: Saturday, May 09, 2020 2:43 PM
To: Joyal, André
Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

Dear Andr'e,

> By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
> The dream of a formal system in which every proof leads to an actual computation may be far off.
> Not that we should abandon it, new discoveries are always possible.
> Is there a version of type theory for proving and verifying, less
> for computing?

In my opinion the currenrly implemented type theories are essentially
for proving and not for computing.
But if you haven't mechanized PART of equational reasoning it would be
much much more painful than it still is.
But that is "only" a pragmatic issue.

> The notations of type theory are very useful in homotopy theory.
> But the absence of simplicial types is a serious obstacle to applications.

In cubical type theory they sort of live well with cubes not being
fibrant... They have them as pretypes. But maybe I misunderstand...

Thomas

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

* Re: [HoTT] Identity versus equality
2020-05-09 20:18                                  Joyal, André
@ 2020-05-09 21:27                                    Jon Sterling
2020-05-10  2:19                                      Joyal, André
2020-05-10 11:46                                      Thorsten Altenkirch
2020-05-10 12:53                                    Ulrik Buchholtz
2020-05-10 16:51                                    Nicolai Kraus
2 siblings, 2 replies; 61+ messages in thread
From: Jon Sterling @ 2020-05-09 21:27 UTC (permalink / raw)
To: 'Martin Escardo' via Homotopy Type Theory

Dear André,

The coherence problems involved in formulating everyday notions like simplicial types (what an amazing world we live in to be able to call this everyday!) can be resolved by extending Homotopy Type Theory with a "sub-homotopical" layer, a second equality type that is meant to capture the strict mathematical equality instead of paths. This is sometimes called Two Level Type Theory. In this case, it is possible to define simplicial types, using the strict equality to sidestep the problem of defining homotopy coherent structures in HoTT.

There are a number of ways to achieve this, and they have different tradeoffs depending on what your goals are. The space of possible realizations of this idea corresponds to what Thomas has referred to as the "subjectivity" of judgmental equality.

Best,
Jon

On Sat, May 9, 2020, at 4:18 PM, Joyal, André wrote:
> Dear Thomas,
>
> You wrote
>
> <<In my opinion the currenrly implemented type theories are essentially
> for proving and not for computing.
> But if you haven't mechanized PART of equational reasoning it would be
> much much more painful than it still is.
> But that is "only" a pragmatic issue.>>
>
> Type  theory has very nice features. I wish they could be preserved and
> developped further.
> But I find it frustrating that I cant do my everyday mathematics with
> it.
> For example, I cannot  say
>
> (1) Let X:\Delta^{op}---->Type be a simplicial type;
> (2) Let G be a type equipped with a group structure;
> (3) Let BG be the classifying space of a group G;
> (4) Let Gr be the category of groups;
> (5) Let SType be the category of simplical types.
> (6) Let Map(X,Y) be the simplicial types of maps X--->Y
> between two simplicial types X and Y.
>
> It is crucial to have (1)
> For example, a group could be defined to
> be a simplicial object satisfying the Segal conditions.
> The classifying space of a group is the colimit of this simplicial object.
> The category of groups can be defined to be
> a simplicial objects satisfiying the Rezk conditions (a complete Segal space).
>
> Is there some aspects of type theory that we may give up as a price
> for solving these problems ?
>
>
> Best,
> André
>
> ________________________________________
> Sent: Saturday, May 09, 2020 2:43 PM
> To: Joyal, André
> Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey;
> Subject: Re: [HoTT] Identity versus equality
>
> Dear Andr'e,
>
> > By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
> > The dream of a formal system in which every proof leads to an actual computation may be far off.
> > Not that we should abandon it, new discoveries are always possible.
> > Is there a version of type theory for proving and verifying, less
> > for computing?
>
> In my opinion the currenrly implemented type theories are essentially
> for proving and not for computing.
> But if you haven't mechanized PART of equational reasoning it would be
> much much more painful than it still is.
> But that is "only" a pragmatic issue.
>
> > The notations of type theory are very useful in homotopy theory.
> > But the absence of simplicial types is a serious obstacle to applications.
>
> In cubical type theory they sort of live well with cubes not being
> fibrant... They have them as pretypes. But maybe I misunderstand...
>
> 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
> To view this discussion on the web visit
>

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

* RE: [HoTT] Identity versus equality
2020-05-09 21:27                                    Jon Sterling
@ 2020-05-10  2:19                                      Joyal, André
2020-05-10  3:04                                        Jon Sterling
2020-05-10 11:46                                      Thorsten Altenkirch
From: Joyal, André @ 2020-05-10  2:19 UTC (permalink / raw)
To: Jon Sterling, 'Martin Escardo' via Homotopy Type Theory

Dear Jon,

You wrote:

<<The coherence problems involved in formulating everyday notions like simplicial types (what an amazing world we live in to be able to call this everyday!) can be resolved by extending Homotopy Type Theory with a "sub-homotopical" layer, a second equality type that is meant to capture the strict mathematical equality instead of paths.>>

That is interesting.
Is the "strict" equality like the equality relation between the maps of a Quillen model structure?
I am curious to see the description of such a formal system.

Is it related to Vladimir's theory with 3 levels of equality (which I never understood)?

Best,
André

________________________________________
Sent: Saturday, May 09, 2020 5:27 PM
To: 'Martin Escardo' via Homotopy Type Theory
Subject: Re: [HoTT] Identity versus equality

Dear André,

The coherence problems involved in formulating everyday notions like simplicial types (what an amazing world we live in to be able to call this everyday!) can be resolved by extending Homotopy Type Theory with a "sub-homotopical" layer, a second equality type that is meant to capture the strict mathematical equality instead of paths. This is sometimes called Two Level Type Theory. In this case, it is possible to define simplicial types, using the strict equality to sidestep the problem of defining homotopy coherent structures in HoTT.

There are a number of ways to achieve this, and they have different tradeoffs depending on what your goals are. The space of possible realizations of this idea corresponds to what Thomas has referred to as the "subjectivity" of judgmental equality.

Best,
Jon

On Sat, May 9, 2020, at 4:18 PM, Joyal, André wrote:
> Dear Thomas,
>
> You wrote
>
> <<In my opinion the currenrly implemented type theories are essentially
> for proving and not for computing.
> But if you haven't mechanized PART of equational reasoning it would be
> much much more painful than it still is.
> But that is "only" a pragmatic issue.>>
>
> Type  theory has very nice features. I wish they could be preserved and
> developped further.
> But I find it frustrating that I cant do my everyday mathematics with
> it.
> For example, I cannot  say
>
> (1) Let X:\Delta^{op}---->Type be a simplicial type;
> (2) Let G be a type equipped with a group structure;
> (3) Let BG be the classifying space of a group G;
> (4) Let Gr be the category of groups;
> (5) Let SType be the category of simplical types.
> (6) Let Map(X,Y) be the simplicial types of maps X--->Y
> between two simplicial types X and Y.
>
> It is crucial to have (1)
> For example, a group could be defined to
> be a simplicial object satisfying the Segal conditions.
> The classifying space of a group is the colimit of this simplicial object.
> The category of groups can be defined to be
> a simplicial objects satisfiying the Rezk conditions (a complete Segal space).
>
> Is there some aspects of type theory that we may give up as a price
> for solving these problems ?
>
>
> Best,
> André
>
> ________________________________________
> Sent: Saturday, May 09, 2020 2:43 PM
> To: Joyal, André
> Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey;
> Subject: Re: [HoTT] Identity versus equality
>
> Dear Andr'e,
>
> > By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
> > The dream of a formal system in which every proof leads to an actual computation may be far off.
> > Not that we should abandon it, new discoveries are always possible.
> > Is there a version of type theory for proving and verifying, less
> > for computing?
>
> In my opinion the currenrly implemented type theories are essentially
> for proving and not for computing.
> But if you haven't mechanized PART of equational reasoning it would be
> much much more painful than it still is.
> But that is "only" a pragmatic issue.
>
> > The notations of type theory are very useful in homotopy theory.
> > But the absence of simplicial types is a serious obstacle to applications.
>
> In cubical type theory they sort of live well with cubes not being
> fibrant... They have them as pretypes. But maybe I misunderstand...
>
> 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
> To view this discussion on the web visit
>

--
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/b1d32ac0-e364-4405-9e48-e0e1e0b37732%40www.fastmail.com.

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

* Re: [HoTT] Identity versus equality
2020-05-10  2:19                                      Joyal, André
@ 2020-05-10  3:04                                        Jon Sterling
2020-05-10  9:09                                          Thomas Streicher
From: Jon Sterling @ 2020-05-10  3:04 UTC (permalink / raw)
To: "Joyal, André"
Cc: 'Martin Escardo' via Homotopy Type Theory

Dear André,

I don’t want to accidentally say the wrong thing, I think your intuition about the quillen model category is correct. Let me just say that the strict equality of the type theory is interpreted as the mathematical equality of a 1-categorical presentation of an infinity category, for instance mathematical equality of cells in a simplicial set. The “homotopical semantics” of type theory currently always factor through some 1-categorical presentation of an infinity category (some may wish to change this! I welcome it); judgmental equality is at present always “about” the 1-categorical presentation, whereas path equality is intended to only make distinctions that makes sense at the level of the infinity-categorical localization.

I am somewhat familiar with Vladimir’s HTS (Homotopy Type System) — the arrangement is that you have judgmental equality, a “strict equality” type, and a path type. Some types are distinguished as fibrant and others are not — for instance, the fibrant types are closed under path types but not strict equality types. A rule is added to ensure that the judgmental equality coincides with the (inhabitedness of the) strict equality type — this rule is called “equality reflection” by the logicians and type theorists. The rules are arranged to ensure that strict equality implies path equality but not the other way around. This ensured by having a notion of non-fibrant type (rather than having all types be fibrant).

This may sound very confusing, but for intuitions it is helpful to think of what it means in the context of an “intended model” (for instance, Vladimir’s model in simplicial sets). In that case, there is an object that weakly classifies *all* small simplicial sets, and there is also an object that weakly classifies just the Kan-fibrant small simplicial sets. The HTS formalism is then a (very strict) language to capture the general-abstract aspects of this semantic situation.

Vladimir’s HTS can be thought of as extending Martin-L\”of’s Extensional Type Theory with homotopical notions; this is particularly natural from a mathematical point of view, considering that a quillen model category usually has finite limits. Other authors have considered realizations of this idea that are more like extending Martin-L\”of’s Intensional Type Theory + Streicher’s Axiom K with homotopical notions (where Axiom K is something to ensure that there can, up to identity, be only one proof of a given identity); this style is preferred for implementation or computational purposes. The differences between these points of view are more syntactic than semantic — I would call them “subjective” in deference to Thomas.

Best,
Jon

> On May 9, 2020, at 10:19 PM, Joyal, André <joyal...@uqam.ca> wrote:
>
> Dear Jon,
>
> You wrote:
>
> <<The coherence problems involved in formulating everyday notions like simplicial types (what an amazing world we live in to be able to call this everyday!) can be resolved by extending Homotopy Type Theory with a "sub-homotopical" layer, a second equality type that is meant to capture the strict mathematical equality instead of paths.>>
>
> That is interesting.
> Is the "strict" equality like the equality relation between the maps of a Quillen model structure?
> I am curious to see the description of such a formal system.
>
> Is it related to Vladimir's theory with 3 levels of equality (which I never understood)?
>
> Best,
> André
>
> ________________________________________
> Sent: Saturday, May 09, 2020 5:27 PM
> To: 'Martin Escardo' via Homotopy Type Theory
> Subject: Re: [HoTT] Identity versus equality
>
> Dear André,
>
> The coherence problems involved in formulating everyday notions like simplicial types (what an amazing world we live in to be able to call this everyday!) can be resolved by extending Homotopy Type Theory with a "sub-homotopical" layer, a second equality type that is meant to capture the strict mathematical equality instead of paths. This is sometimes called Two Level Type Theory. In this case, it is possible to define simplicial types, using the strict equality to sidestep the problem of defining homotopy coherent structures in HoTT.
>
> There are a number of ways to achieve this, and they have different tradeoffs depending on what your goals are. The space of possible realizations of this idea corresponds to what Thomas has referred to as the "subjectivity" of judgmental equality.
>
> Best,
> Jon
>
>
> On Sat, May 9, 2020, at 4:18 PM, Joyal, André wrote:
>> Dear Thomas,
>>
>> You wrote
>>
>> <<In my opinion the currenrly implemented type theories are essentially
>> for proving and not for computing.
>> But if you haven't mechanized PART of equational reasoning it would be
>> much much more painful than it still is.
>> But that is "only" a pragmatic issue.>>
>>
>> Type  theory has very nice features. I wish they could be preserved and
>> developped further.
>> But I find it frustrating that I cant do my everyday mathematics with
>> it.
>> For example, I cannot  say
>>
>> (1) Let X:\Delta^{op}---->Type be a simplicial type;
>> (2) Let G be a type equipped with a group structure;
>> (3) Let BG be the classifying space of a group G;
>> (4) Let Gr be the category of groups;
>> (5) Let SType be the category of simplical types.
>> (6) Let Map(X,Y) be the simplicial types of maps X--->Y
>> between two simplicial types X and Y.
>>
>> It is crucial to have (1)
>> For example, a group could be defined to
>> be a simplicial object satisfying the Segal conditions.
>> The classifying space of a group is the colimit of this simplicial object.
>> The category of groups can be defined to be
>> a simplicial objects satisfiying the Rezk conditions (a complete Segal space).
>>
>> Is there some aspects of type theory that we may give up as a price
>> for solving these problems ?
>>
>>
>> Best,
>> André
>>
>> ________________________________________
>> Sent: Saturday, May 09, 2020 2:43 PM
>> To: Joyal, André
>> Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey;
>> Subject: Re: [HoTT] Identity versus equality
>>
>> Dear Andr'e,
>>
>>> By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
>>> The dream of a formal system in which every proof leads to an actual computation may be far off.
>>> Not that we should abandon it, new discoveries are always possible.
>>> Is there a version of type theory for proving and verifying, less
>>> for computing?
>>
>> In my opinion the currenrly implemented type theories are essentially
>> for proving and not for computing.
>> But if you haven't mechanized PART of equational reasoning it would be
>> much much more painful than it still is.
>> But that is "only" a pragmatic issue.
>>
>>> The notations of type theory are very useful in homotopy theory.
>>> But the absence of simplicial types is a serious obstacle to applications.
>>
>> In cubical type theory they sort of live well with cubes not being
>> fibrant... They have them as pretypes. But maybe I misunderstand...
>>
>> 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
>> To view this discussion on the web visit
>>
>
> --
> 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/b1d32ac0-e364-4405-9e48-e0e1e0b37732%40www.fastmail.com.

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

* Re: [HoTT] Identity versus equality
2020-05-10  3:04                                        Jon Sterling
@ 2020-05-10  9:09                                          Thomas Streicher
2020-05-10 11:59                                            Thorsten Altenkirch
From: Thomas Streicher @ 2020-05-10  9:09 UTC (permalink / raw)
To: Jon Sterling
Cc: "Joyal, André",
'Martin Escardo' via Homotopy Type Theory

Dear Andr'e and Jon,

I mostly agree with what Jon said. I also think that intensional type
theory within an extensional type theory (it is 2 levels and not 3) is
an attractive system for cubical type theory.
In the simplicial case this is a bit more problematic since the
filling conditions for Kan complexes involve classical existential
quantification and as shown by Thierry et.al. this is important!

That the extensional level is just formulated using J and K is a
possibility. It has to be seen in practice how far it goes.

Let me finish with a remark on how constructive traditional topos
theory is. I don't mean the logic represented by a topos but which
logical principles one uses when doing topos theory.
Since one wants to develop toposes relative to fairly general base
toposes people introduced fibered/indexed reasoning. But the reasoning
about fibrations is per se fairly classical and also involves choice
for classes typically. So this reasoning is performed on a meta level
and not within the logic of the base topos. For the situations when
this is partly possible Benabou invented the notion of "definability".

This is sometimes swept under the carpet because of some "antilogical"
tendencies which were influential at the time of the genesis of topos
theory (beautifully described in a little essay by Reyes I recnely
found on his home page). I am aware that I am on dangerous grounds now
since Andr'e has really experienced and shaped these days (when I
started high school).
But it coincides with my impression of what is the practice of the
working topos theorist...

I think the real antagonism is or was that those days (and I am afraid
world view. This has changed recently where even among set theorists
there is a "multiverse" and a "universe" fraction and the former is
getting larger compared to the past. This is funny in a sense since
one of the reasons for a multiverse veiw was independnce results is
set theory...

Anyway both traditional topos theory and higher dimensional category
theory was and is developed within a unrestricted metatheory which
could be formalized in ZFC + every set is an element of some Grothendieck universe.

It is not impossible that certain aspects and fragments can be
developed in weaker systems but there is no guarantee that this will
always work.

Thomas

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

* Re: [HoTT] Identity versus equality
2020-05-09 21:27                                    Jon Sterling
2020-05-10  2:19                                      Joyal, André
@ 2020-05-10 11:46                                      Thorsten Altenkirch
2020-05-10 14:01                                        Michael Shulman
From: Thorsten Altenkirch @ 2020-05-10 11:46 UTC (permalink / raw)
To: Jon Sterling, 'Martin Escardo' via Homotopy Type Theory

Hi Jon,

I just had an exchange with Andre regarding this which I forgot to cc to the list.

Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type (actually you can do it as a coinductive definition). You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.

However, presheaves over Delta cannot be written as a Reedy limit. Now there are a number of ways to address this. We can work with semi-simplicial sets and add Hornfillers by stating equivalences (there is no coherence problem because these are propositional). To regain identities we can add the assumption that the higher category is univalent (i.e. for every object the type of objects paired with an equivalence is contractible) which entails the existence of degeneracies.

The question of how to define simplicial types remains however. I find that looking at the lower levels of simplicial presheaves it is actually strange that binary composition is handled via horn-fillers whlle identity, i.e. nullary composition, is built into the structure. Maybe we should treat identity in the same way as composition, which means that we introduce a family modelling degeneracies.

What I mean is that if we write down the first levels of a semisimplicial type we have

X0 : U
X1 : X0 -> X0 -> U
X2 : (x0,x1,x2 : X0) -> X0 x0 x1 -> X0 x1 x2 -> X0 x0 x2 -> U

But we can add degeneracies by adding families which say that some object is a degeneracy:

I0 : (x0 : X0) -> X1 x0 x0 -> U
I1_0 : (x0 x1 : X0)(f : X1 x0 x1)(i : X1 x0 x0) -> I0 x0 i -> X2 x0 x1 x1 i f f -> U
I1_1 : (x0 x1 : X0)(f : X1 x0 x1)(i : X1 x1 x1) -> I0 x1 i -> X2 x0 x0 x1 f i f -> U

That is while X2 can be viewed as a proof-relevant predicate that a triangle commutes, I0 is a predicate that an arrow is an identity and I1_0 , I1_1 are predicates that triangles are degenerate.

Adding horn-fillers type-theoretically corresponds to saying that certain types are contractible:

(x0,x1,x2 : X0)(f : X1 x0 x1)(g : X1 x1 x2) -> is-contractible ((h : X1 x0 x2) \times X2 x0 x1 x2 f g h)

where is-contractible(A) = (a : A) \times ((x : A) -> a = x)

(x0 : X0) -> is-contractible (X1 x0 x0)
(x0 x1 : X0)(f : X1 x0 x1)(i : X1 x0 x0)(j : I0 x0 i) -> is-contractible ((x :  X2 x0 x1 x1 i f f) \times I1_0 x0 x1 f i j x)
(x0 x1 : X0)(f : X1 x0 x1)(i : X1 x1 x1)(j : I0 x0 i) -> is-contractible ((x :  X2 x0 x0 x1 f i f) \times I1_0 x1 x1 f i j x)

This is related to Kraus' & Sattler's directed replacement:
https://arxiv.org/abs/1704.04543

Andre mentioned that degeneracies play an important role in the classical theory of simplicial sets, e.g. to show that geometric realisation preserves finite limits. However, the situation is quote different here because we work with types not sets. Hence you would expect that the topologies are also higher-dimensional objects. Has anybody looked at this?

Thorsten

﻿On 09/05/2020, 22:28, "homotopyt...@googlegroups.com on behalf of Jon Sterling" <homotopyt...@googlegroups.com on behalf of j...@jonmsterling.com> wrote:

Dear André,

The coherence problems involved in formulating everyday notions like simplicial types (what an amazing world we live in to be able to call this everyday!) can be resolved by extending Homotopy Type Theory with a "sub-homotopical" layer, a second equality type that is meant to capture the strict mathematical equality instead of paths. This is sometimes called Two Level Type Theory. In this case, it is possible to define simplicial types, using the strict equality to sidestep the problem of defining homotopy coherent structures in HoTT.

There are a number of ways to achieve this, and they have different tradeoffs depending on what your goals are. The space of possible realizations of this idea corresponds to what Thomas has referred to as the "subjectivity" of judgmental equality.

Best,
Jon

On Sat, May 9, 2020, at 4:18 PM, Joyal, André wrote:
> Dear Thomas,
>
> You wrote
>
> <<In my opinion the currenrly implemented type theories are essentially
> for proving and not for computing.
> But if you haven't mechanized PART of equational reasoning it would be
> much much more painful than it still is.
> But that is "only" a pragmatic issue.>>
>
> Type  theory has very nice features. I wish they could be preserved and
> developped further.
> But I find it frustrating that I cant do my everyday mathematics with
> it.
> For example, I cannot  say
>
> (1) Let X:\Delta^{op}---->Type be a simplicial type;
> (2) Let G be a type equipped with a group structure;
> (3) Let BG be the classifying space of a group G;
> (4) Let Gr be the category of groups;
> (5) Let SType be the category of simplical types.
> (6) Let Map(X,Y) be the simplicial types of maps X--->Y
> between two simplicial types X and Y.
>
> It is crucial to have (1)
> For example, a group could be defined to
> be a simplicial object satisfying the Segal conditions.
> The classifying space of a group is the colimit of this simplicial object.
> The category of groups can be defined to be
> a simplicial objects satisfiying the Rezk conditions (a complete Segal space).
>
> Is there some aspects of type theory that we may give up as a price
> for solving these problems ?
>
>
> Best,
> André
>
> ________________________________________
> Sent: Saturday, May 09, 2020 2:43 PM
> To: Joyal, André
> Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey;
> Subject: Re: [HoTT] Identity versus equality
>
> Dear Andr'e,
>
> > By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
> > The dream of a formal system in which every proof leads to an actual computation may be far off.
> > Not that we should abandon it, new discoveries are always possible.
> > Is there a version of type theory for proving and verifying, less
> > for computing?
>
> In my opinion the currenrly implemented type theories are essentially
> for proving and not for computing.
> But if you haven't mechanized PART of equational reasoning it would be
> much much more painful than it still is.
> But that is "only" a pragmatic issue.
>
> > The notations of type theory are very useful in homotopy theory.
> > But the absence of simplicial types is a serious obstacle to applications.
>
> In cubical type theory they sort of live well with cubes not being
> fibrant... They have them as pretypes. But maybe I misunderstand...
>
> 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
> To view this discussion on the web visit
>

--
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/b1d32ac0-e364-4405-9e48-e0e1e0b37732%40www.fastmail.com.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
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] 61+ messages in thread

* Re: [HoTT] Identity versus equality
2020-05-10  9:09                                          Thomas Streicher
@ 2020-05-10 11:59                                            Thorsten Altenkirch
0 siblings, 0 replies; 61+ messages in thread
From: Thorsten Altenkirch @ 2020-05-10 11:59 UTC (permalink / raw)
To: Thomas Streicher, Jon Sterling
Cc: "Joyal, André",
'Martin Escardo' via Homotopy Type Theory

Dear Thomas,

I mostly agree with what Jon said. I also think that intensional type
theory within an extensional type theory (it is 2 levels and not 3) is
an attractive system for cubical type theory.

That seems to be putting the cart before the horse. HoTT is the theory I want to work in, the strict layer is only there to do some internalized metatheory.

In the simplicial case this is a bit more problematic since the
filling conditions for Kan complexes involve classical existential
quantification and as shown by Thierry et.al. this is important!

I think we have two discussions here: one is about simplicial sets which is about the reduction of HoTT to set level structures and the other is about (semi-)simplicial types which is about modelling higher structures within HoTT.

The classical assumptions in the filling conditions for Kan complexes can be avoided as was shown by Gambino and Sattler:
https://arxiv.org/abs/1510.00669
who develop a theory of uniform fibrations that captures both cubical and simplicial sets. This means we can model Pi-types using uniform simplicial sets. However, it is not clear how to interpret a univalent universe in uniform simplicial sets. It is possible to do this in uniform cubical sets due to the fact that the interval is a tiny object.

That the extensional level is just formulated using J and K is a
possibility. It has to be seen in practice how far it goes.

You need K on the strict level, because that is exactly the point that you don’t need to care about coherences anymore. Btw, I think calling it "extensional level" is a misnomer because actually the fibrant layer is more extensional than the strict one because it is univalent.

So for example if you define semi-simplicial types in a 2-level type theory it is essential that you have K.

Cheers,
Thorsten

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
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] 61+ messages in thread

* Re: [HoTT] Identity versus equality
2020-05-09 20:18                                  Joyal, André
2020-05-09 21:27                                    Jon Sterling
@ 2020-05-10 12:53                                    Ulrik Buchholtz
2020-05-10 14:01                                      Michael Shulman
2020-05-10 18:04                                      Joyal, André
2020-05-10 16:51                                    Nicolai Kraus
2 siblings, 2 replies; 61+ messages in thread
From: Ulrik Buchholtz @ 2020-05-10 12:53 UTC (permalink / raw)
To: Homotopy Type Theory

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

Dear André,

On Saturday, May 9, 2020 at 10:18:11 PM UTC+2, joyal wrote:

> But I find it frustrating that I cant do my everyday mathematics with it.
>
> For example, I cannot  say
>
> (1) Let X:\Delta^{op}---->Type be a simplicial type;
>

Let me remind everyone that we don't have a proof that it's impossible to
define simplicial types in book HoTT! As long as we haven't settled this
question either way, the predicament we're in (and I agree it's a
predicament) is more an indictment of type theorists than of type theory.
(And I include myself as a type theorist here.)

Anyway, from your phrasing of (1), it looks like you're after a directed
type theory. Several groups are working on type theories where your (1) is
valid syntax, but you have to write Space (or Anima or ...) to indicate the
covariant universe of homotopy types and maps, rather than the full
universe.

(2) Let G be a type equipped with a group structure;
>
(3) Let BG be the classifying space of a group G;
> (4) Let Gr be the category of groups;
>

Again, let me remind everyone, that groups are precisely one of the few
structures we know how to handle (along with grouplike E_n-types, and
connective/general spectra): To equip a type G with a group structure is to
give a pointed connected type BG and an equivalence of G with the loop type
of BG. The type of objects of Gr is the universe of pointed, connected
types.

When you replace groups by monoids, it gets more embarrassing.

Earlier (on May 7) you wrote:

> At some level, all mathematics is based on some kind of set theory.
> Is it not obvious?
> We cannot escape Cantor's paradise!
>

That is exactly the question, isn't it?

What HoTT/UF offers us is another axis of foundational variation, besides
the old classical/constructive, impredicative/predicative,
infinitist/finitist, namely: everything is based on sets/general homotopy
types are not reducible to sets.

I don't know of catchy names for these positions, but I think that working
with HoTT has a tendency of making the latter position more plausible: Why
should there for any type be a set that surjects onto it?

A question: Recall that if we assume the axiom of choice (AC) for sets,
then there is a surjection from a set onto Set, namely the map that takes a
cardinal (or ordinal) to the set of ordinals below it.
Is there (with AC for sets) also a surjection from a set to the type of
1-types? To the full universe?

The 2-level type theories can be viewed as another way of making a type
theory that is faithful to the idea that everything is based on sets. I
like to think of the outer layer as an exoskeleton for type theory, giving
it a bit of extra strength while we don't know how to use its own powers
fully, or whether indeed it is strong enough to effect constructions like
that of simplicial types. Every type (which for me is a fibrant type, since
that's the mathematically meaningful ones) has a corresponding exotype
(indeed an exoset), but there are more exotypes, such as the exonatural
numbers, which are sometimes useful.

Best wishes,
Ulrik

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

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

* Re: [HoTT] Identity versus equality
2020-05-10 12:53                                    Ulrik Buchholtz
@ 2020-05-10 14:01                                      Michael Shulman
2020-05-10 14:27                                        Nicolai Kraus
2020-05-10 18:04                                      Joyal, André
From: Michael Shulman @ 2020-05-10 14:01 UTC (permalink / raw)
To: Ulrik Buchholtz; +Cc: Homotopy Type Theory

On Sun, May 10, 2020 at 5:53 AM Ulrik Buchholtz
<ulrikbu...@gmail.com> wrote:
> What HoTT/UF offers us is another axis of foundational variation, besides the old classical/constructive, impredicative/predicative, infinitist/finitist, namely: everything is based on sets/general homotopy types are not reducible to sets.

Exactly!

> A question: Recall that if we assume the axiom of choice (AC) for sets, then there is a surjection from a set onto Set, namely the map that takes a cardinal (or ordinal) to the set of ordinals below it.
> Is there (with AC for sets) also a surjection from a set to the type of 1-types? To the full universe?

As far as I know, it is an open question whether AC for sets implies
these stronger principles (although I'd be surprised if it were true).
Those principles are true, of course, in the model of simplicial sets
based on ZFC, and there are models in which they fail, but I don't
know of a model in which they fail but AC for sets holds.  Although I
don't think I've really tried to look for one either; has anyone?

There is however the theorem stated at
https://ncatlab.org/nlab/show/n-types+cover#relation_to_other_axioms,
that AC for sets together with the axiom "every type is surjected onto
by a set" is equivalent to the "oo-AC" that "every surjection onto a
set has a section".

> The 2-level type theories can be viewed as another way of making a type theory that is faithful to the idea that everything is based on sets.

While I kind of see how one could say this, I think it's misleading
especially in light of the above dichotomy, becuase 2LTT doesn't imply
any of the *internal* "types are based on sets" axioms for the fibrant
layer.  As you know, 2LTT without additional axioms is conservative
over HoTT, while even with stronger axioms it can still be modeled in
many or all higher toposes.

> I like to think of the outer layer as an exoskeleton for type theory, giving it a bit of extra strength while we don't know how to use its own powers fully, or whether indeed it is strong enough to effect constructions like that of simplicial types. Every type (which for me is a fibrant type, since that's the mathematically meaningful ones) has a corresponding exotype (indeed an exoset), but there are more exotypes, such as the exonatural numbers, which are sometimes useful.

I think "exo-" is a great prefix for the outer layer!

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

* Re: [HoTT] Identity versus equality
2020-05-10 11:46                                      Thorsten Altenkirch
@ 2020-05-10 14:01                                        Michael Shulman
2020-05-10 14:20                                          Nicolai Kraus
2020-05-10 19:20                                          Thorsten Altenkirch
0 siblings, 2 replies; 61+ messages in thread
From: Michael Shulman @ 2020-05-10 14:01 UTC (permalink / raw)
To: Thorsten Altenkirch
Cc: Jon Sterling, 'Martin Escardo' via Homotopy Type Theory

On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type

We can certainly *talk* about simplicial types in 2LTT as exofunctors
from the exocategory Delta to the exocategory Type.  I assume the
point you're making is that we don't have a (fibrant) *type of*
simplicial types, whereas we do have a fibrant type of semisimplicial
types (under appropriate axioms)?

> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.

Personally, I think the best axiom to use here is that exo-Nat is
*cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy.  We
don't know how to model "exo-Nat is fibrant" in all higher toposes,
but it's easy to interpret "exo-Nat is cofibrant" in such models,
since Pi-types with domain exo-Nat are just externally-infinite
products.

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

* Re: [HoTT] Identity versus equality
2020-05-10 14:01                                        Michael Shulman
@ 2020-05-10 14:20                                          Nicolai Kraus
2020-05-10 14:34                                            Michael Shulman
2020-05-10 19:20                                          Thorsten Altenkirch
From: Nicolai Kraus @ 2020-05-10 14:20 UTC (permalink / raw)
To: Michael Shulman, Thorsten Altenkirch
Cc: Jon Sterling, 'Martin Escardo' via Homotopy Type Theory

On 10/05/2020 15:01, Michael Shulman wrote:
> On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
> <Thorsten....@nottingham.ac.uk> wrote:
>> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type
> We can certainly *talk* about simplicial types in 2LTT as exofunctors
> from the exocategory Delta to the exocategory Type.  I assume the
> point you're making is that we don't have a (fibrant) *type of*
> simplicial types, whereas we do have a fibrant type of semisimplicial
> types (under appropriate axioms)?

Judging from the rest of his message, I believe that Thorsten was
talking about the direct replacement construction in Christian's and my
abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant",
this gives us a fibrant type that one could call "simplicial types" (and
Thorsten does). But of course it's an encoding. If we decide to use such
encodings, I fear we may lose the main advantage that the "axiomatic"
representations in HoTT have, namely avoiding encodings. (I mean the
bisimplicial sets.)

>> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.
> Personally, I think the best axiom to use here is that exo-Nat is
> *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy.  We
> don't know how to model "exo-Nat is fibrant" in all higher toposes,
> but it's easy to interpret "exo-Nat is cofibrant" in such models,
> since Pi-types with domain exo-Nat are just externally-infinite
> products.

I completely agree with your preference for this axiom :-)
But Thorsten does has a point if we consider the "engineering level"
that was discussed earlier in this thread. Allowing coinductive types
with exo-Nat as an index makes it possible to use your paper (Higher
Stucture Identity Principle, arXiv:2004.06572) and get a construction of
semi-simplicial types which is more convenient to use in a proof assistant.

-- Nicolai

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

* Re: [HoTT] Identity versus equality
2020-05-10 14:01                                      Michael Shulman
@ 2020-05-10 14:27                                        Nicolai Kraus
2020-05-10 15:35                                          Ulrik Buchholtz
From: Nicolai Kraus @ 2020-05-10 14:27 UTC (permalink / raw)
To: Michael Shulman; +Cc: Ulrik Buchholtz, Homotopy Type Theory

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

On Sun, May 10, 2020 at 3:01 PM Michael Shulman <shu...@sandiego.edu>
wrote:

> On Sun, May 10, 2020 at 5:53 AM Ulrik Buchholtz
> <ulrikbu...@gmail.com> wrote:
> > The 2-level type theories can be viewed as another way of making a type
> theory that is faithful to the idea that everything is based on sets.
>
> While I kind of see how one could say this, I think it's misleading
> especially in light of the above dichotomy, becuase 2LTT doesn't imply
> any of the *internal* "types are based on sets" axioms for the fibrant
> layer.  As you know, 2LTT without additional axioms is conservative
> over HoTT, while even with stronger axioms it can still be modeled in
> many or all higher toposes.
>

I agree with Mike - sorry Ulrik :-)
For me, "everything is based on sets" would mean that every fibrant type
can be written as the realization of a (semi-) simplicial type, or
something like this.

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

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

* Re: [HoTT] Identity versus equality
2020-05-10 14:20                                          Nicolai Kraus
@ 2020-05-10 14:34                                            Michael Shulman
2020-05-10 14:52                                              Nicolai Kraus
2020-05-10 19:15                                              Thorsten Altenkirch
0 siblings, 2 replies; 61+ messages in thread
From: Michael Shulman @ 2020-05-10 14:34 UTC (permalink / raw)
To: Nicolai Kraus
Cc: Thorsten Altenkirch, Jon Sterling,
'Martin Escardo' via Homotopy Type Theory

Many or all coinductive types can be constructed, at least up to
equivalence, using Pi-types and (some kind of) Nat.  Is there any
chance that "exo-Nat is cofibrant" could be used to justify the
existence/fibrancy of the coinductive types you want?

On Sun, May 10, 2020 at 7:20 AM Nicolai Kraus <nicola...@gmail.com> wrote:
>
> On 10/05/2020 15:01, Michael Shulman wrote:
> > On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
> > <Thorsten....@nottingham.ac.uk> wrote:
> >> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type
> > We can certainly *talk* about simplicial types in 2LTT as exofunctors
> > from the exocategory Delta to the exocategory Type.  I assume the
> > point you're making is that we don't have a (fibrant) *type of*
> > simplicial types, whereas we do have a fibrant type of semisimplicial
> > types (under appropriate axioms)?
>
> Judging from the rest of his message, I believe that Thorsten was
> talking about the direct replacement construction in Christian's and my
> abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant",
> this gives us a fibrant type that one could call "simplicial types" (and
> Thorsten does). But of course it's an encoding. If we decide to use such
> encodings, I fear we may lose the main advantage that the "axiomatic"
> representations in HoTT have, namely avoiding encodings. (I mean the
> bisimplicial sets.)
>
> >> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.
> > Personally, I think the best axiom to use here is that exo-Nat is
> > *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy.  We
> > don't know how to model "exo-Nat is fibrant" in all higher toposes,
> > but it's easy to interpret "exo-Nat is cofibrant" in such models,
> > since Pi-types with domain exo-Nat are just externally-infinite
> > products.
>
> I completely agree with your preference for this axiom :-)
> But Thorsten does has a point if we consider the "engineering level"
> that was discussed earlier in this thread. Allowing coinductive types
> with exo-Nat as an index makes it possible to use your paper (Higher
> Stucture Identity Principle, arXiv:2004.06572) and get a construction of
> semi-simplicial types which is more convenient to use in a proof assistant.
>
> -- Nicolai

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

* Re: [HoTT] Identity versus equality
2020-05-10 14:34                                            Michael Shulman
@ 2020-05-10 14:52                                              Nicolai Kraus
2020-05-10 15:16                                                Michael Shulman
2020-05-10 19:15                                              Thorsten Altenkirch
From: Nicolai Kraus @ 2020-05-10 14:52 UTC (permalink / raw)
To: Michael Shulman
Cc: Thorsten Altenkirch, Jon Sterling,
'Martin Escardo' via Homotopy Type Theory

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

I would guess that "exo-Nat is cofibrant" justifies the coinductive type in
question, but not its judgmental computation rules. And the judgmental
computation rules are probably the very reason why one would want this
coinductive type. But this is just a guess.
-- Nicolai

On Sun, May 10, 2020 at 3:35 PM Michael Shulman <shu...@sandiego.edu>
wrote:

> Many or all coinductive types can be constructed, at least up to
> equivalence, using Pi-types and (some kind of) Nat.  Is there any
> chance that "exo-Nat is cofibrant" could be used to justify the
> existence/fibrancy of the coinductive types you want?
>
> On Sun, May 10, 2020 at 7:20 AM Nicolai Kraus <nicola...@gmail.com>
> wrote:
> >
> > On 10/05/2020 15:01, Michael Shulman wrote:
> > > On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
> > > <Thorsten....@nottingham.ac.uk> wrote:
> > >> Defining simplicial types isn't entirely straightforward (as you know
> I suppose), because Delta is not directed. We can do semi-simplicial types
> as a Reedy limit, i.e. an infinite Sigma type
> > > We can certainly *talk* about simplicial types in 2LTT as exofunctors
> > > from the exocategory Delta to the exocategory Type.  I assume the
> > > point you're making is that we don't have a (fibrant) *type of*
> > > simplicial types, whereas we do have a fibrant type of semisimplicial
> > > types (under appropriate axioms)?
> >
> > Judging from the rest of his message, I believe that Thorsten was
> > talking about the direct replacement construction in Christian's and my
> > abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant",
> > this gives us a fibrant type that one could call "simplicial types" (and
> > Thorsten does). But of course it's an encoding. If we decide to use such
> > encodings, I fear we may lose the main advantage that the "axiomatic"
> > representations in HoTT have, namely avoiding encodings. (I mean the
> > "main advantage" of HoTT compared to traditional approaches, e.g. taking
> > bisimplicial sets.)
> >
> > >> You need some extra principles, e.g. that strict Nat is fibrant or
> maybe better that certain coinductive types exist.
> > > Personally, I think the best axiom to use here is that exo-Nat is
> > > *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy.  We
> > > don't know how to model "exo-Nat is fibrant" in all higher toposes,
> > > but it's easy to interpret "exo-Nat is cofibrant" in such models,
> > > since Pi-types with domain exo-Nat are just externally-infinite
> > > products.
> >
> > I completely agree with your preference for this axiom :-)
> > But Thorsten does has a point if we consider the "engineering level"
> > that was discussed earlier in this thread. Allowing coinductive types
> > with exo-Nat as an index makes it possible to use your paper (Higher
> > Stucture Identity Principle, arXiv:2004.06572) and get a construction of
> > semi-simplicial types which is more convenient to use in a proof
> assistant.
> >
> > -- Nicolai
>

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

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

* Re: [HoTT] Identity versus equality
2020-05-10 14:52                                              Nicolai Kraus
@ 2020-05-10 15:16                                                Michael Shulman
2020-05-10 15:23                                                  Nicolai Kraus
From: Michael Shulman @ 2020-05-10 15:16 UTC (permalink / raw)
To: Nicolai Kraus
Cc: Thorsten Altenkirch, Jon Sterling,
'Martin Escardo' via Homotopy Type Theory

I forget -- does "exo-Nat is cofibrant" imply that exo-limits of
towers of fibrations are fibrant?  That's another useful axiom that
holds in models and might make it easier to construct coinductive
types with judgmental computation rules.

On Sun, May 10, 2020 at 7:52 AM Nicolai Kraus <nicola...@gmail.com> wrote:
>
> I would guess that "exo-Nat is cofibrant" justifies the coinductive type in question, but not its judgmental computation rules. And the judgmental computation rules are probably the very reason why one would want this coinductive type. But this is just a guess.
> -- Nicolai
>
> On Sun, May 10, 2020 at 3:35 PM Michael Shulman <shu...@sandiego.edu> wrote:
>>
>> Many or all coinductive types can be constructed, at least up to
>> equivalence, using Pi-types and (some kind of) Nat.  Is there any
>> chance that "exo-Nat is cofibrant" could be used to justify the
>> existence/fibrancy of the coinductive types you want?
>>
>> On Sun, May 10, 2020 at 7:20 AM Nicolai Kraus <nicola...@gmail.com> wrote:
>> >
>> > On 10/05/2020 15:01, Michael Shulman wrote:
>> > > On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
>> > > <Thorsten....@nottingham.ac.uk> wrote:
>> > >> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type
>> > > We can certainly *talk* about simplicial types in 2LTT as exofunctors
>> > > from the exocategory Delta to the exocategory Type.  I assume the
>> > > point you're making is that we don't have a (fibrant) *type of*
>> > > simplicial types, whereas we do have a fibrant type of semisimplicial
>> > > types (under appropriate axioms)?
>> >
>> > Judging from the rest of his message, I believe that Thorsten was
>> > talking about the direct replacement construction in Christian's and my
>> > abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant",
>> > this gives us a fibrant type that one could call "simplicial types" (and
>> > Thorsten does). But of course it's an encoding. If we decide to use such
>> > encodings, I fear we may lose the main advantage that the "axiomatic"
>> > representations in HoTT have, namely avoiding encodings. (I mean the
>> > "main advantage" of HoTT compared to traditional approaches, e.g. taking
>> > bisimplicial sets.)
>> >
>> > >> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.
>> > > Personally, I think the best axiom to use here is that exo-Nat is
>> > > *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy.  We
>> > > don't know how to model "exo-Nat is fibrant" in all higher toposes,
>> > > but it's easy to interpret "exo-Nat is cofibrant" in such models,
>> > > since Pi-types with domain exo-Nat are just externally-infinite
>> > > products.
>> >
>> > I completely agree with your preference for this axiom :-)
>> > But Thorsten does has a point if we consider the "engineering level"
>> > that was discussed earlier in this thread. Allowing coinductive types
>> > with exo-Nat as an index makes it possible to use your paper (Higher
>> > Stucture Identity Principle, arXiv:2004.06572) and get a construction of
>> > semi-simplicial types which is more convenient to use in a proof assistant.
>> >
>> > -- 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/CA%2BAZBBr0Zh-uLfEZCXUapK5KHFDxkzxyvLW22zyjmrB8KmWtYQ%40mail.gmail.com.

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

* Re: [HoTT] Identity versus equality
2020-05-10 15:16                                                Michael Shulman
@ 2020-05-10 15:23                                                  Nicolai Kraus
2020-05-10 16:13                                                    Nicolai Kraus
From: Nicolai Kraus @ 2020-05-10 15:23 UTC (permalink / raw)
To: Michael Shulman
Cc: Thorsten Altenkirch, Jon Sterling,
'Martin Escardo' via Homotopy Type Theory

Yes, I think that is one main motivation for this axiom (that you've
suggested in this form :-) and I also believe that it was Vladimir's
main motivation for his axiom "exo-Nat is fibrant". I think the two
axioms really serve the same purpose, but the "cofibrant" version is
much more harmless.

On 10/05/2020 16:16, Michael Shulman wrote:
> I forget -- does "exo-Nat is cofibrant" imply that exo-limits of
> towers of fibrations are fibrant?  That's another useful axiom that
> holds in models and might make it easier to construct coinductive
> types with judgmental computation rules.
>
> On Sun, May 10, 2020 at 7:52 AM Nicolai Kraus <nicola...@gmail.com> wrote:
>> I would guess that "exo-Nat is cofibrant" justifies the coinductive type in question, but not its judgmental computation rules. And the judgmental computation rules are probably the very reason why one would want this coinductive type. But this is just a guess.
>> -- Nicolai
>>
>> On Sun, May 10, 2020 at 3:35 PM Michael Shulman <shu...@sandiego.edu> wrote:
>>> Many or all coinductive types can be constructed, at least up to
>>> equivalence, using Pi-types and (some kind of) Nat.  Is there any
>>> chance that "exo-Nat is cofibrant" could be used to justify the
>>> existence/fibrancy of the coinductive types you want?
>>>
>>> On Sun, May 10, 2020 at 7:20 AM Nicolai Kraus <nicola...@gmail.com> wrote:
>>>> On 10/05/2020 15:01, Michael Shulman wrote:
>>>>> On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
>>>>> <Thorsten....@nottingham.ac.uk> wrote:
>>>>>> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type
>>>>> We can certainly *talk* about simplicial types in 2LTT as exofunctors
>>>>> from the exocategory Delta to the exocategory Type.  I assume the
>>>>> point you're making is that we don't have a (fibrant) *type of*
>>>>> simplicial types, whereas we do have a fibrant type of semisimplicial
>>>>> types (under appropriate axioms)?
>>>> Judging from the rest of his message, I believe that Thorsten was
>>>> talking about the direct replacement construction in Christian's and my
>>>> abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant",
>>>> this gives us a fibrant type that one could call "simplicial types" (and
>>>> Thorsten does). But of course it's an encoding. If we decide to use such
>>>> encodings, I fear we may lose the main advantage that the "axiomatic"
>>>> representations in HoTT have, namely avoiding encodings. (I mean the
>>>> bisimplicial sets.)
>>>>
>>>>>> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.
>>>>> Personally, I think the best axiom to use here is that exo-Nat is
>>>>> *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy.  We
>>>>> don't know how to model "exo-Nat is fibrant" in all higher toposes,
>>>>> but it's easy to interpret "exo-Nat is cofibrant" in such models,
>>>>> since Pi-types with domain exo-Nat are just externally-infinite
>>>>> products.
>>>> I completely agree with your preference for this axiom :-)
>>>> But Thorsten does has a point if we consider the "engineering level"
>>>> that was discussed earlier in this thread. Allowing coinductive types
>>>> with exo-Nat as an index makes it possible to use your paper (Higher
>>>> Stucture Identity Principle, arXiv:2004.06572) and get a construction of
>>>> semi-simplicial types which is more convenient to use in a proof assistant.
>>>>
>>>> -- 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/CA%2BAZBBr0Zh-uLfEZCXUapK5KHFDxkzxyvLW22zyjmrB8KmWtYQ%40mail.gmail.com.

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

* Re: [HoTT] Identity versus equality
2020-05-10 14:27                                        Nicolai Kraus
@ 2020-05-10 15:35                                          Ulrik Buchholtz
2020-05-10 16:30                                            Michael Shulman
2020-05-10 18:56                                            Nicolai Kraus
0 siblings, 2 replies; 61+ messages in thread
From: Ulrik Buchholtz @ 2020-05-10 15:35 UTC (permalink / raw)
To: Homotopy Type Theory

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

On Sunday, May 10, 2020 at 4:27:30 PM UTC+2, Nicolai Kraus wrote:
>
> I agree with Mike - sorry Ulrik :-)
> For me, "everything is based on sets" would mean that every fibrant type
> can be written as the realization of a (semi-) simplicial type, or
> something like this.
>

No need to apologize: I know I was being slightly provocative by
juxtaposing a question about sets cover (SC) and a comment on 2-level type
theory in this context, in order to provoke some discussion :-)

Wouldn't you agree, however, that even though basic 2LTT is conservative
over HoTT, from a certain point of view, 2LTT privileges the “ground floor”
exosets? In your very nice paper, https://arxiv.org/abs/1705.03307, you
decorate the inner (fibrant, endo-) types as special, and leave the
exotypes undecorated, privileging the latter. While from a user's
perspective, however, it's the (inner) types that are
standard/mathematical, and the exotypes that are special.

And regardless of the decorations, the mere fact that we bring in the
exoset level makes the theory harder to justify from the philosophical
position that general homotopy types are not reducible to sets. One can in
fact see the conservativity result as foundational reduction (in the sense
of https://math.stanford.edu/~feferman/papers/reductive.pdf section 5) from
a system justified by the principle that everything is based on sets to a
system justified by a framework where that isn't the case.

Another connection is that it seems it should be easier to find an axiom,
which might imply SC, that would allow us to construct the type of
semi-simplicial types, rather than such an axiom that doesn't imply SC. But
I don't know any such axiom statable in book HoTT either way.

BTW, you probably meant “simplicial set” above. And yes, that kind of axiom
would be the strongest expression of “everything is based sets”, and it
currently needs 2LTT to even be stated.

Cheers,
Ulrik

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

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

* Re: [HoTT] Identity versus equality
2020-05-10 15:23                                                  Nicolai Kraus
@ 2020-05-10 16:13                                                    Nicolai Kraus
2020-05-10 16:28                                                      Michael Shulman
From: Nicolai Kraus @ 2020-05-10 16:13 UTC (permalink / raw)
To: Michael Shulman
Cc: Thorsten Altenkirch, Jon Sterling,
'Martin Escardo' via Homotopy Type Theory

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

I have to correct what I said an hour ago (thanks, Mike). We don't know
whether "exo-Nat is cofibrant" implies that exo-limits of towers are
fibrant. (And probably it doesn't.)
In other words, we don't know the connection between axioms (A2) and (A3)
in arXiv:1705.03307.
-- Nicolai

On Sun, May 10, 2020 at 4:23 PM Nicolai Kraus <nicola...@gmail.com>
wrote:

> Yes, I think that is one main motivation for this axiom (that you've
> suggested in this form :-) and I also believe that it was Vladimir's
> main motivation for his axiom "exo-Nat is fibrant". I think the two
> axioms really serve the same purpose, but the "cofibrant" version is
> much more harmless.
>
> On 10/05/2020 16:16, Michael Shulman wrote:
> > I forget -- does "exo-Nat is cofibrant" imply that exo-limits of
> > towers of fibrations are fibrant?  That's another useful axiom that
> > holds in models and might make it easier to construct coinductive
> > types with judgmental computation rules.
> >
> > On Sun, May 10, 2020 at 7:52 AM Nicolai Kraus <nicola...@gmail.com>
> wrote:
> >> I would guess that "exo-Nat is cofibrant" justifies the coinductive
> type in question, but not its judgmental computation rules. And the
> judgmental computation rules are probably the very reason why one would
> want this coinductive type. But this is just a guess.
> >> -- Nicolai
> >>
> >> On Sun, May 10, 2020 at 3:35 PM Michael Shulman <shu...@sandiego.edu>
> wrote:
> >>> Many or all coinductive types can be constructed, at least up to
> >>> equivalence, using Pi-types and (some kind of) Nat.  Is there any
> >>> chance that "exo-Nat is cofibrant" could be used to justify the
> >>> existence/fibrancy of the coinductive types you want?
> >>>
> >>> On Sun, May 10, 2020 at 7:20 AM Nicolai Kraus <nicola...@gmail.com>
> wrote:
> >>>> On 10/05/2020 15:01, Michael Shulman wrote:
> >>>>> On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
> >>>>> <Thorsten....@nottingham.ac.uk> wrote:
> >>>>>> Defining simplicial types isn't entirely straightforward (as you
> know I suppose), because Delta is not directed. We can do semi-simplicial
> types as a Reedy limit, i.e. an infinite Sigma type
> >>>>> We can certainly *talk* about simplicial types in 2LTT as exofunctors
> >>>>> from the exocategory Delta to the exocategory Type.  I assume the
> >>>>> point you're making is that we don't have a (fibrant) *type of*
> >>>>> simplicial types, whereas we do have a fibrant type of semisimplicial
> >>>>> types (under appropriate axioms)?
> >>>> Judging from the rest of his message, I believe that Thorsten was
> >>>> talking about the direct replacement construction in Christian's and
> my
> >>>> abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant",
> >>>> this gives us a fibrant type that one could call "simplicial types"
> (and
> >>>> Thorsten does). But of course it's an encoding. If we decide to use
> such
> >>>> encodings, I fear we may lose the main advantage that the "axiomatic"
> >>>> representations in HoTT have, namely avoiding encodings. (I mean the
> taking
> >>>> bisimplicial sets.)
> >>>>
> >>>>>> You need some extra principles, e.g. that strict Nat is fibrant or
> maybe better that certain coinductive types exist.
> >>>>> Personally, I think the best axiom to use here is that exo-Nat is
> >>>>> *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy.  We
> >>>>> don't know how to model "exo-Nat is fibrant" in all higher toposes,
> >>>>> but it's easy to interpret "exo-Nat is cofibrant" in such models,
> >>>>> since Pi-types with domain exo-Nat are just externally-infinite
> >>>>> products.
> >>>> I completely agree with your preference for this axiom :-)
> >>>> But Thorsten does has a point if we consider the "engineering level"
> >>>> that was discussed earlier in this thread. Allowing coinductive types
> >>>> with exo-Nat as an index makes it possible to use your paper (Higher
> >>>> Stucture Identity Principle, arXiv:2004.06572) and get a construction
> of
> >>>> semi-simplicial types which is more convenient to use in a proof
> assistant.
> >>>>
> >>>> -- 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
> >> To view this discussion on the web visit
> .
>
>

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

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

* Re: [HoTT] Identity versus equality
2020-05-10 16:13                                                    Nicolai Kraus
@ 2020-05-10 16:28                                                      Michael Shulman
2020-05-10 18:18                                                        Nicolai Kraus
From: Michael Shulman @ 2020-05-10 16:28 UTC (permalink / raw)

Okay.  But the implication works in the other way, doesn't it?  A
product indexed by exo-Nat is the exo-limit of a tower of finite
products.  So maybe the tower axiom is the best one.

On Sun, May 10, 2020 at 9:13 AM Nicolai Kraus <nicola...@gmail.com> wrote:
>
> I have to correct what I said an hour ago (thanks, Mike). We don't know whether "exo-Nat is cofibrant" implies that exo-limits of towers are fibrant. (And probably it doesn't.)
> In other words, we don't know the connection between axioms (A2) and (A3) in arXiv:1705.03307.
>  -- Nicolai
>
> On Sun, May 10, 2020 at 4:23 PM Nicolai Kraus <nicola...@gmail.com> wrote:
>>
>> Yes, I think that is one main motivation for this axiom (that you've
>> suggested in this form :-) and I also believe that it was Vladimir's
>> main motivation for his axiom "exo-Nat is fibrant". I think the two
>> axioms really serve the same purpose, but the "cofibrant" version is
>> much more harmless.
>>
>> On 10/05/2020 16:16, Michael Shulman wrote:
>> > I forget -- does "exo-Nat is cofibrant" imply that exo-limits of
>> > towers of fibrations are fibrant?  That's another useful axiom that
>> > holds in models and might make it easier to construct coinductive
>> > types with judgmental computation rules.
>> >
>> > On Sun, May 10, 2020 at 7:52 AM Nicolai Kraus <nicola...@gmail.com> wrote:
>> >> I would guess that "exo-Nat is cofibrant" justifies the coinductive type in question, but not its judgmental computation rules. And the judgmental computation rules are probably the very reason why one would want this coinductive type. But this is just a guess.
>> >> -- Nicolai
>> >>
>> >> On Sun, May 10, 2020 at 3:35 PM Michael Shulman <shu...@sandiego.edu> wrote:
>> >>> Many or all coinductive types can be constructed, at least up to
>> >>> equivalence, using Pi-types and (some kind of) Nat.  Is there any
>> >>> chance that "exo-Nat is cofibrant" could be used to justify the
>> >>> existence/fibrancy of the coinductive types you want?
>> >>>
>> >>> On Sun, May 10, 2020 at 7:20 AM Nicolai Kraus <nicola...@gmail.com> wrote:
>> >>>> On 10/05/2020 15:01, Michael Shulman wrote:
>> >>>>> On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
>> >>>>> <Thorsten....@nottingham.ac.uk> wrote:
>> >>>>>> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type
>> >>>>> We can certainly *talk* about simplicial types in 2LTT as exofunctors
>> >>>>> from the exocategory Delta to the exocategory Type.  I assume the
>> >>>>> point you're making is that we don't have a (fibrant) *type of*
>> >>>>> simplicial types, whereas we do have a fibrant type of semisimplicial
>> >>>>> types (under appropriate axioms)?
>> >>>> Judging from the rest of his message, I believe that Thorsten was
>> >>>> talking about the direct replacement construction in Christian's and my
>> >>>> abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant",
>> >>>> this gives us a fibrant type that one could call "simplicial types" (and
>> >>>> Thorsten does). But of course it's an encoding. If we decide to use such
>> >>>> encodings, I fear we may lose the main advantage that the "axiomatic"
>> >>>> representations in HoTT have, namely avoiding encodings. (I mean the
>> >>>> "main advantage" of HoTT compared to traditional approaches, e.g. taking
>> >>>> bisimplicial sets.)
>> >>>>
>> >>>>>> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.
>> >>>>> Personally, I think the best axiom to use here is that exo-Nat is
>> >>>>> *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy.  We
>> >>>>> don't know how to model "exo-Nat is fibrant" in all higher toposes,
>> >>>>> but it's easy to interpret "exo-Nat is cofibrant" in such models,
>> >>>>> since Pi-types with domain exo-Nat are just externally-infinite
>> >>>>> products.
>> >>>> I completely agree with your preference for this axiom :-)
>> >>>> But Thorsten does has a point if we consider the "engineering level"
>> >>>> that was discussed earlier in this thread. Allowing coinductive types
>> >>>> with exo-Nat as an index makes it possible to use your paper (Higher
>> >>>> Stucture Identity Principle, arXiv:2004.06572) and get a construction of
>> >>>> semi-simplicial types which is more convenient to use in a proof assistant.
>> >>>>
>> >>>> -- 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/CA%2BAZBBr0Zh-uLfEZCXUapK5KHFDxkzxyvLW22zyjmrB8KmWtYQ%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/CA%2BAZBBrJF92OezfqYyh9vy-JQNesC8%2BpacAPPrq-xDZN5Y6qNQ%40mail.gmail.com.

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

* Re: [HoTT] Identity versus equality
2020-05-10 15:35                                          Ulrik Buchholtz
@ 2020-05-10 16:30                                            Michael Shulman
2020-05-10 18:56                                            Nicolai Kraus
1 sibling, 0 replies; 61+ messages in thread
From: Michael Shulman @ 2020-05-10 16:30 UTC (permalink / raw)
To: Ulrik Buchholtz; +Cc: Homotopy Type Theory

I realize this may be controversial too, but I think there's at least
one sense in which sets are "more fundamental", namely that ordinary
syntax consists of sets, because it is a (non-higher) inductive type.
I think this is kind of the "reason" for the conservativity theorem.

I don't think this fact detracts from the importance and independence
of the homotopical point of view, any more than the fact that (say)
finite sets have decidable equality detracts from the importance of
constructivism.  It's just the fact that simpler things are simpler.

On Sun, May 10, 2020 at 8:35 AM Ulrik Buchholtz
<ulrikbu...@gmail.com> wrote:
>
> On Sunday, May 10, 2020 at 4:27:30 PM UTC+2, Nicolai Kraus wrote:
>>
>> I agree with Mike - sorry Ulrik :-)
>> For me, "everything is based on sets" would mean that every fibrant type can be written as the realization of a (semi-) simplicial type, or something like this.
>
>
> No need to apologize: I know I was being slightly provocative by juxtaposing a question about sets cover (SC) and a comment on 2-level type theory in this context, in order to provoke some discussion :-)
>
> Wouldn't you agree, however, that even though basic 2LTT is conservative over HoTT, from a certain point of view, 2LTT privileges the “ground floor” exosets? In your very nice paper, https://arxiv.org/abs/1705.03307, you decorate the inner (fibrant, endo-) types as special, and leave the exotypes undecorated, privileging the latter. While from a user's perspective, however, it's the (inner) types that are standard/mathematical, and the exotypes that are special.
>
> And regardless of the decorations, the mere fact that we bring in the exoset level makes the theory harder to justify from the philosophical position that general homotopy types are not reducible to sets. One can in fact see the conservativity result as foundational reduction (in the sense of https://math.stanford.edu/~feferman/papers/reductive.pdf section 5) from a system justified by the principle that everything is based on sets to a system justified by a framework where that isn't the case.
>
> Another connection is that it seems it should be easier to find an axiom, which might imply SC, that would allow us to construct the type of semi-simplicial types, rather than such an axiom that doesn't imply SC. But I don't know any such axiom statable in book HoTT either way.
>
> BTW, you probably meant “simplicial set” above. And yes, that kind of axiom would be the strongest expression of “everything is based sets”, and it currently needs 2LTT to even be stated.
>
> Cheers,
> Ulrik
>
> --
> 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.

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

* Re: [HoTT] Identity versus equality
2020-05-09 20:18                                  Joyal, André
2020-05-09 21:27                                    Jon Sterling
2020-05-10 12:53                                    Ulrik Buchholtz
@ 2020-05-10 16:51                                    Nicolai Kraus
2020-05-10 18:57                                      Michael Shulman
2020-05-10 19:18                                      Nicolai Kraus
2 siblings, 2 replies; 61+ messages in thread
From: Nicolai Kraus @ 2020-05-10 16:51 UTC (permalink / raw)
To: Joyal, André, Thomas Streicher
Cc: David Roberts, Thorsten Altenkirch, Michael Shulman,

Dear André and everyone,

I feel it's worth pointing out that there are two strategies to express
"everyday mathematics" in HoTT. In CS-speak, they would probably be
called "shallow embedding" and "deep embedding". Shallow embedding is
the "HoTT style", deep embedding is the "pre-HoTT type theory style".
Shallow means that one uses that the host language shares structure with
the object one wants to define, while deep means one doesn't. To explain
what I mean, let's look at the type theoretic definition of a group (a
1-group, not a higher group).

Definition using deep embedding: A group is a tuple
(X,h,e,o,i,assoc,...), where
X : Type     -- carrier
h : is-0-truncated(X)     -- carrier is set
e : X   -- unit
o : X * X -> X     -- composition
i : X -> X     -- inverses
assoc : (h o g) o f = h o (g o f)
... [and so on]

Definition using shallow embedding: A group is a pointed connected 1-type.

Fortunately, these definitions are equivalent (via the Eilenberg-McLan
spaces construction). But they behave differently when we want to work
with them or change them. It's easy to change the second definition to
define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 ,
arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there
is a nice way for the first definition. The second definition has better
computational properties than the first.

When you say this:

> But I find it frustrating that I cant do my everyday mathematics with it.
> For example, I cannot  say
>
> (1) Let X:\Delta^{op}---->Type be a simplicial type;

You are referring to shallow embedding. In everyday mathematics, you
don't say (1) either. You probably say (1) with "Type" replaced by "Set"
or by "simplicial set". Both of these can be expressed straightforwardly
in type theory using only (h-)sets (i.e. embedding deeply).

We strive to use shallow embedding as often as possible for the reasons
in the above example. But let's assume that we *can* say (1) in HoTT,
using "Type", because we find some encoding that we're reasonably happy
with; there's a question which I've asked myself before:

Will we not destroy the advantages of deep (over shallow) embedding if
we fall back to encodings (and thus destroy the main selling point of
HoTT)? For me, the justification of still using deep embedding is that
statements using encodings (e.g. "the universe is a higher category)
might still imply statements which don't use encodings and are
interesting. However, if we want to develop a theory of certain higher
structures for it's own sake, then it's not so clear to me whether it's
really better to use the HoTT-style deep embedding.

Kind regards,
Nicolai

On 09/05/2020 21:18, Joyal, André wrote:
> Dear Thomas,
>
> You wrote
>
> <<In my opinion the currenrly implemented type theories are essentially
> for proving and not for computing.
> But if you haven't mechanized PART of equational reasoning it would be
> much much more painful than it still is.
> But that is "only" a pragmatic issue.>>
>
> Type  theory has very nice features. I wish they could be preserved and developped further.
> But I find it frustrating that I cant do my everyday mathematics with it.
> For example, I cannot  say
>
> (1) Let X:\Delta^{op}---->Type be a simplicial type;
> (2) Let G be a type equipped with a group structure;
> (3) Let BG be the classifying space of a group G;
> (4) Let Gr be the category of groups;
> (5) Let SType be the category of simplical types.
> (6) Let Map(X,Y) be the simplicial types of maps X--->Y
> between two simplicial types X and Y.
>
> It is crucial to have (1)
> For example, a group could be defined to
> be a simplicial object satisfying the Segal conditions.
> The classifying space of a group is the colimit of this simplicial object.
> The category of groups can be defined to be
> a simplicial objects satisfiying the Rezk conditions (a complete Segal space).
>
> Is there some aspects of type theory that we may give up as a price
> for solving these problems ?
>
>
> Best,
> André
>
> ________________________________________
> Sent: Saturday, May 09, 2020 2:43 PM
> To: Joyal, André
> Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
> Subject: Re: [HoTT] Identity versus equality
>
> Dear Andr'e,
>
>> By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
>> The dream of a formal system in which every proof leads to an actual computation may be far off.
>> Not that we should abandon it, new discoveries are always possible.
>> Is there a version of type theory for proving and verifying, less
>> for computing?
> In my opinion the currenrly implemented type theories are essentially
> for proving and not for computing.
> But if you haven't mechanized PART of equational reasoning it would be
> much much more painful than it still is.
> But that is "only" a pragmatic issue.
>
>> The notations of type theory are very useful in homotopy theory.
>> But the absence of simplicial types is a serious obstacle to applications.
> In cubical type theory they sort of live well with cubes not being
> fibrant... They have them as pretypes. But maybe I misunderstand...
>
> Thomas
>

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

* RE: [HoTT] Identity versus equality
2020-05-10 12:53                                    Ulrik Buchholtz
2020-05-10 14:01                                      Michael Shulman
@ 2020-05-10 18:04                                      Joyal, André
2020-05-11  7:33                                        Thomas Streicher
From: Joyal, André @ 2020-05-10 18:04 UTC (permalink / raw)
To: Ulrik Buchholtz, Homotopy Type Theory

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

Dear Ulrik,

You wrote:

<<The 2-level type theories can be viewed as another way of making a type theory that is faithful to the idea that everything is based on sets. I like to think of the outer layer as an exoskeleton for type theory, giving it a bit of extra strength while we don't know how to use its own powers fully, or whether indeed it is strong enough to effect constructions like that of simplicial types. Every type (which for me is a fibrant type, since that's the mathematically meaningful ones) has a corresponding exotype (indeed an exoset), but there are more exotypes, such as the exonatural numbers, which are sometimes useful.>>

I like the idea of calling exo-skeleton the outer layer of a type theory.
Category theorists like to distinguish between the internal and the external properties of a category.
Logician are distinguishing a formal theory from its meta-theory.
A theory and its meta-theory may interact as in Gödel's incompleteness theorem.
There are two layers interacting in ML type theory.
Is it possible to interpret the outer layer internally, as in Gödel's incompleteness theorem?

You wrote:

<<Again, let me remind everyone, that groups are precisely one of the few structures we know how to handle (along with grouplike E_n-types, and connective/general spectra): To equip a type G with a group structure is to give a pointed connected type BG and an equivalence of G with the loop type of BG. The type of objects of Gr is the universe of pointed, connected types.>>

I like the idea of studying groups via the equivalence between groups and pointed connected spaces.
It is one of the great miracle of homotopy theory (discovered by Kan).
It is quite amazing if you think about it: (non-abelian) groups were introduced for the purpose
of studying symmetries, mostly in Galois theory. The fundamental group of a space was introduced
by Poincaré to study covering spaces in connection with the Klein-Poincaré
uniformisation theorem for Riemann surfaces. The loop space of a pointed space
is a kind of beef-up version of the fundamental group; the fact that it contains
all the homotopy invariant informations about that space is a great marvel.
Topologists are interested in nilpotent groups (ex. the work of Hilton) and
the connection with Lie algebras (the Whitehead bracket).
By a theorem of Quillen, connected differential graded Lie algebras are rational models of simply connected spaces.
Also, in Goodwillie's calculus, the derivative of the identity functor is the Lie algebra operad.

I am afraid the equivalence between groups and pointed connected spaces
will be meaningless (tautological) if the former is defined to be the latter.

Best,
André

________________________________
Sent: Sunday, May 10, 2020 8:53 AM
To: Homotopy Type Theory
Subject: Re: [HoTT] Identity versus equality

Dear André,

On Saturday, May 9, 2020 at 10:18:11 PM UTC+2, joyal wrote:
But I find it frustrating that I cant do my everyday mathematics with it.

For example, I cannot  say

(1) Let X:\Delta^{op}---->Type be a simplicial type;

Let me remind everyone that we don't have a proof that it's impossible to define simplicial types in book HoTT! As long as we haven't settled this question either way, the predicament we're in (and I agree it's a predicament) is more an indictment of type theorists than of type theory. (And I include myself as a type theorist here.)

Anyway, from your phrasing of (1), it looks like you're after a directed type theory. Several groups are working on type theories where your (1) is valid syntax, but you have to write Space (or Anima or ...) to indicate the covariant universe of homotopy types and maps, rather than the full universe.

(2) Let G be a type equipped with a group structure;

(3) Let BG be the classifying space of a group G;
(4) Let Gr be the category of groups;

Again, let me remind everyone, that groups are precisely one of the few structures we know how to handle (along with grouplike E_n-types, and connective/general spectra): To equip a type G with a group structure is to give a pointed connected type BG and an equivalence of G with the loop type of BG. The type of objects of Gr is the universe of pointed, connected types.

When you replace groups by monoids, it gets more embarrassing.

Earlier (on May 7) you wrote:
At some level, all mathematics is based on some kind of set theory.
Is it not obvious?

That is exactly the question, isn't it?

What HoTT/UF offers us is another axis of foundational variation, besides the old classical/constructive, impredicative/predicative, infinitist/finitist, namely: everything is based on sets/general homotopy types are not reducible to sets.

I don't know of catchy names for these positions, but I think that working with HoTT has a tendency of making the latter position more plausible: Why should there for any type be a set that surjects onto it?

A question: Recall that if we assume the axiom of choice (AC) for sets, then there is a surjection from a set onto Set, namely the map that takes a cardinal (or ordinal) to the set of ordinals below it.
Is there (with AC for sets) also a surjection from a set to the type of 1-types? To the full universe?

The 2-level type theories can be viewed as another way of making a type theory that is faithful to the idea that everything is based on sets. I like to think of the outer layer as an exoskeleton for type theory, giving it a bit of extra strength while we don't know how to use its own powers fully, or whether indeed it is strong enough to effect constructions like that of simplicial types. Every type (which for me is a fibrant type, since that's the mathematically meaningful ones) has a corresponding exotype (indeed an exoset), but there are more exotypes, such as the exonatural numbers, which are sometimes useful.

Best wishes,
Ulrik

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

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

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

* Re: [HoTT] Identity versus equality
2020-05-10 16:28                                                      Michael Shulman
@ 2020-05-10 18:18                                                        Nicolai Kraus
0 siblings, 0 replies; 61+ messages in thread
From: Nicolai Kraus @ 2020-05-10 18:18 UTC (permalink / raw)

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

Yes, this is nice. We should add it to the next revision of the paper
(arXiv:1705.03307).

On Sun, May 10, 2020 at 5:29 PM Michael Shulman <shu...@sandiego.edu>
wrote:

> Okay.  But the implication works in the other way, doesn't it?  A
> product indexed by exo-Nat is the exo-limit of a tower of finite
> products.  So maybe the tower axiom is the best one.
>
> On Sun, May 10, 2020 at 9:13 AM Nicolai Kraus <nicola...@gmail.com>
> wrote:
> >
> > I have to correct what I said an hour ago (thanks, Mike). We don't know
> whether "exo-Nat is cofibrant" implies that exo-limits of towers are
> fibrant. (And probably it doesn't.)
> > In other words, we don't know the connection between axioms (A2) and
> (A3) in arXiv:1705.03307.
> >  -- Nicolai
> >
> > On Sun, May 10, 2020 at 4:23 PM Nicolai Kraus <nicola...@gmail.com>
> wrote:
> >>
> >> Yes, I think that is one main motivation for this axiom (that you've
> >> suggested in this form :-) and I also believe that it was Vladimir's
> >> main motivation for his axiom "exo-Nat is fibrant". I think the two
> >> axioms really serve the same purpose, but the "cofibrant" version is
> >> much more harmless.
> >>
> >> On 10/05/2020 16:16, Michael Shulman wrote:
> >> > I forget -- does "exo-Nat is cofibrant" imply that exo-limits of
> >> > towers of fibrations are fibrant?  That's another useful axiom that
> >> > holds in models and might make it easier to construct coinductive
> >> > types with judgmental computation rules.
> >> >
> >> > On Sun, May 10, 2020 at 7:52 AM Nicolai Kraus <
> nicola...@gmail.com> wrote:
> >> >> I would guess that "exo-Nat is cofibrant" justifies the coinductive
> type in question, but not its judgmental computation rules. And the
> judgmental computation rules are probably the very reason why one would
> want this coinductive type. But this is just a guess.
> >> >> -- Nicolai
> >> >>
> >> >> On Sun, May 10, 2020 at 3:35 PM Michael Shulman <
> shu...@sandiego.edu> wrote:
> >> >>> Many or all coinductive types can be constructed, at least up to
> >> >>> equivalence, using Pi-types and (some kind of) Nat.  Is there any
> >> >>> chance that "exo-Nat is cofibrant" could be used to justify the
> >> >>> existence/fibrancy of the coinductive types you want?
> >> >>>
> >> >>> On Sun, May 10, 2020 at 7:20 AM Nicolai Kraus <
> nicola...@gmail.com> wrote:
> >> >>>> On 10/05/2020 15:01, Michael Shulman wrote:
> >> >>>>> On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
> >> >>>>> <Thorsten....@nottingham.ac.uk> wrote:
> >> >>>>>> Defining simplicial types isn't entirely straightforward (as you
> know I suppose), because Delta is not directed. We can do semi-simplicial
> types as a Reedy limit, i.e. an infinite Sigma type
> >> >>>>> We can certainly *talk* about simplicial types in 2LTT as
> exofunctors
> >> >>>>> from the exocategory Delta to the exocategory Type.  I assume the
> >> >>>>> point you're making is that we don't have a (fibrant) *type of*
> >> >>>>> simplicial types, whereas we do have a fibrant type of
> semisimplicial
> >> >>>>> types (under appropriate axioms)?
> >> >>>> Judging from the rest of his message, I believe that Thorsten was
> >> >>>> talking about the direct replacement construction in Christian's
> and my
> >> >>>> abstract arXiv:1704.04543. With the assumption "exo-Nat is
> cofibrant",
> >> >>>> this gives us a fibrant type that one could call "simplicial
> types" (and
> >> >>>> Thorsten does). But of course it's an encoding. If we decide to
> use such
> >> >>>> encodings, I fear we may lose the main advantage that the
> "axiomatic"
> >> >>>> representations in HoTT have, namely avoiding encodings. (I mean
> the
> >> >>>> "main advantage" of HoTT compared to traditional approaches, e.g.
> taking
> >> >>>> bisimplicial sets.)
> >> >>>>
> >> >>>>>> You need some extra principles, e.g. that strict Nat is fibrant
> or maybe better that certain coinductive types exist.
> >> >>>>> Personally, I think the best axiom to use here is that exo-Nat is
> >> >>>>> *cofibrant*, i.e. Pi-types with domain exo-Nat preserve
> fibrancy.  We
> >> >>>>> don't know how to model "exo-Nat is fibrant" in all higher
> toposes,
> >> >>>>> but it's easy to interpret "exo-Nat is cofibrant" in such models,
> >> >>>>> since Pi-types with domain exo-Nat are just externally-infinite
> >> >>>>> products.
> >> >>>> I completely agree with your preference for this axiom :-)
> >> >>>> But Thorsten does has a point if we consider the "engineering
> level"
> >> >>>> that was discussed earlier in this thread. Allowing coinductive
> types
> >> >>>> with exo-Nat as an index makes it possible to use your paper
> (Higher
> >> >>>> Stucture Identity Principle, arXiv:2004.06572) and get a
> construction of
> >> >>>> semi-simplicial types which is more convenient to use in a proof
> assistant.
> >> >>>>
> >> >>>> -- 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
> .
> >>
> > --
> > 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
> > To view this discussion on the web visit
> .
>
> --
> 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
> To view this discussion on the web visit
> .
>

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

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

* Re: [HoTT] Identity versus equality
2020-05-10 15:35                                          Ulrik Buchholtz
2020-05-10 16:30                                            Michael Shulman
@ 2020-05-10 18:56                                            Nicolai Kraus
1 sibling, 0 replies; 61+ messages in thread
From: Nicolai Kraus @ 2020-05-10 18:56 UTC (permalink / raw)
To: Ulrik Buchholtz; +Cc: Homotopy Type Theory

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

On Sun, May 10, 2020 at 4:35 PM Ulrik Buchholtz <ulrikbu...@gmail.com>
wrote:

> No need to apologize: I know I was being slightly provocative by
> juxtaposing a question about sets cover (SC) and a comment on 2-level type
> theory in this context, in order to provoke some discussion :-)
>

It worked :-)

> Wouldn't you agree, however, that even though basic 2LTT is conservative
> over HoTT, from a certain point of view, 2LTT privileges the “ground floor”
> exosets? In your very nice paper, https://arxiv.org/abs/1705.03307, you
> decorate the inner (fibrant, endo-) types as special, and leave the
> exotypes undecorated, privileging the latter. While from a user's
> perspective, however, it's the (inner) types that are
> standard/mathematical, and the exotypes that are special.
>

I think I see where you are coming from. But for me, decorating the inner
types as special was simply a pragmatic choice, not a philosophical one.
Since most/all statements in the paper are "proper" 2LTT, there are more
exo- / outer types involved than endo- / inner ones. But as a user, one is
interested in the fibrant types (and maybe even assumes that they
coincide with the inner theory), and only adds some small exo-sprinkles
like "exo-Nat is cofibrant"; then, it makes sense to decorate the exo-types
And maybe it would be less confusing if we did the same in the paper that
you linked to. I'm not sure.

> And regardless of the decorations, the mere fact that we bring in the
> exoset level makes the theory harder to justify from the philosophical
> position that general homotopy types are not reducible to sets. One can in
> fact see the conservativity result as foundational reduction (in the sense
> of https://math.stanford.edu/~feferman/papers/reductive.pdf section 5)
> from a system justified by the principle that everything is based on sets
> to a system justified by a framework where that isn't the case.
>

That's interesting, thanks for the link!

> Another connection is that it seems it should be easier to find an axiom,
> which might imply SC, that would allow us to construct the type of
> semi-simplicial types, rather than such an axiom that doesn't imply SC. But
> I don't know any such axiom statable in book HoTT either way.
>

Good question.

> BTW, you probably meant “simplicial set” above. And yes, that kind of
> axiom would be the strongest expression of “everything is based sets”, and
> it currently needs 2LTT to even be stated.
>

You're right, I meant "set". (Otherwise it'd be silly, a type X is the
realization of the [fibrant replacement of] the constant presheaf X.)

Nicolai

> Cheers,
> Ulrik
>
> --
> 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
> To view this discussion on the web visit
> .
>

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

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

* Re: [HoTT] Identity versus equality
2020-05-10 16:51                                    Nicolai Kraus
@ 2020-05-10 18:57                                      Michael Shulman
2020-05-10 19:18                                      Nicolai Kraus
1 sibling, 0 replies; 61+ messages in thread
From: Michael Shulman @ 2020-05-10 18:57 UTC (permalink / raw)
To: Nicolai Kraus
Cc: Joyal, André,
Thomas Streicher, David Roberts, Thorsten Altenkirch,

On Sun, May 10, 2020 at 9:51 AM Nicolai Kraus <nicola...@gmail.com> wrote:
> It's easy to change the second definition to
> define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 ,
> arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there
> is a nice way for the first definition.

On the other hand, it's easy to change the first definition to define
monoids/semigroups/rings/fields/lattices/universal-algebras/etc., and
impossible to do the same for the second.  I think the fact that
groups are part of the general theory of algebraic structures on sets
is more important to incorporate in a definition.  The equivalence
between groups and connected pointed 1-types is better viewed as a
theorem than a definition.

And hence, the "definition" of oo-groups as connected pointed types is
more of a hack than a true definition.  In an ideal world, that would
be a theorem too.  (And the corresponding theorem in classical
mathematics has important content: there are important oo-groupoids
that are obtained by delooping oo-groups nontrivially.)

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

* Re: [HoTT] Identity versus equality
2020-05-10 14:34                                            Michael Shulman
2020-05-10 14:52                                              Nicolai Kraus
@ 2020-05-10 19:15                                              Thorsten Altenkirch
1 sibling, 0 replies; 61+ messages in thread
From: Thorsten Altenkirch @ 2020-05-10 19:15 UTC (permalink / raw)
To: Michael Shulman, nicolai.kraus
Cc: Jon Sterling, 'Martin Escardo' via Homotopy Type Theory,
nicolai.kraus

I thought so but now Nicolai says it is not?

From a type-theoretic point of view it seems more natural to say that indexed M-types are fibrant even if the index is not. Saying that natural numbers are cofibrant assigns a special role to one particular inductive type.

Thorsten

﻿On 10/05/2020, 15:35, "Michael Shulman" <shu...@sandiego.edu> wrote:

Many or all coinductive types can be constructed, at least up to
equivalence, using Pi-types and (some kind of) Nat.  Is there any
chance that "exo-Nat is cofibrant" could be used to justify the
existence/fibrancy of the coinductive types you want?

On Sun, May 10, 2020 at 7:20 AM Nicolai Kraus <nicola...@gmail.com> wrote:
>
> On 10/05/2020 15:01, Michael Shulman wrote:
> > On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
> > <Thorsten....@nottingham.ac.uk> wrote:
> >> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type
> > We can certainly *talk* about simplicial types in 2LTT as exofunctors
> > from the exocategory Delta to the exocategory Type.  I assume the
> > point you're making is that we don't have a (fibrant) *type of*
> > simplicial types, whereas we do have a fibrant type of semisimplicial
> > types (under appropriate axioms)?
>
> Judging from the rest of his message, I believe that Thorsten was
> talking about the direct replacement construction in Christian's and my
> abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant",
> this gives us a fibrant type that one could call "simplicial types" (and
> Thorsten does). But of course it's an encoding. If we decide to use such
> encodings, I fear we may lose the main advantage that the "axiomatic"
> representations in HoTT have, namely avoiding encodings. (I mean the
> bisimplicial sets.)
>
> >> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.
> > Personally, I think the best axiom to use here is that exo-Nat is
> > *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy.  We
> > don't know how to model "exo-Nat is fibrant" in all higher toposes,
> > but it's easy to interpret "exo-Nat is cofibrant" in such models,
> > since Pi-types with domain exo-Nat are just externally-infinite
> > products.
>
> I completely agree with your preference for this axiom :-)
> But Thorsten does has a point if we consider the "engineering level"
> that was discussed earlier in this thread. Allowing coinductive types
> with exo-Nat as an index makes it possible to use your paper (Higher
> Stucture Identity Principle, arXiv:2004.06572) and get a construction of
> semi-simplicial types which is more convenient to use in a proof assistant.
>
> -- Nicolai

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
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] 61+ messages in thread

* Re: [HoTT] Identity versus equality
2020-05-10 16:51                                    Nicolai Kraus
2020-05-10 18:57                                      Michael Shulman
@ 2020-05-10 19:18                                      Nicolai Kraus
2020-05-10 20:22                                        Michael Shulman
From: Nicolai Kraus @ 2020-05-10 19:18 UTC (permalink / raw)
To: Joyal, André, Thomas Streicher
Cc: David Roberts, Thorsten Altenkirch, Michael Shulman,

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

In the last paragraph of my message below, the words "deep" and "shallow"
have to be swapped.

On Sun, May 10, 2020 at 5:51 PM Nicolai Kraus <nicola...@gmail.com>
wrote:

> Dear André and everyone,
>
> I feel it's worth pointing out that there are two strategies to express
> "everyday mathematics" in HoTT. In CS-speak, they would probably be
> called "shallow embedding" and "deep embedding". Shallow embedding is
> the "HoTT style", deep embedding is the "pre-HoTT type theory style".
> Shallow means that one uses that the host language shares structure with
> the object one wants to define, while deep means one doesn't. To explain
> what I mean, let's look at the type theoretic definition of a group (a
> 1-group, not a higher group).
>
> Definition using deep embedding: A group is a tuple
> (X,h,e,o,i,assoc,...), where
>    X : Type     -- carrier
>    h : is-0-truncated(X)     -- carrier is set
>    e : X   -- unit
>    o : X * X -> X     -- composition
>    i : X -> X     -- inverses
>    assoc : (h o g) o f = h o (g o f)
>    ... [and so on]
>
> Definition using shallow embedding: A group is a pointed connected 1-type.
>
> Fortunately, these definitions are equivalent (via the Eilenberg-McLan
> spaces construction). But they behave differently when we want to work
> with them or change them. It's easy to change the second definition to
> define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 ,
> arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there
> is a nice way for the first definition. The second definition has better
> computational properties than the first.
>
> When you say this:
>
>  > But I find it frustrating that I cant do my everyday mathematics with
> it.
>  > For example, I cannot  say
>  >
>  > (1) Let X:\Delta^{op}---->Type be a simplicial type;
>
> You are referring to shallow embedding. In everyday mathematics, you
> don't say (1) either. You probably say (1) with "Type" replaced by "Set"
> or by "simplicial set". Both of these can be expressed straightforwardly
> in type theory using only (h-)sets (i.e. embedding deeply).
>
> We strive to use shallow embedding as often as possible for the reasons
> in the above example. But let's assume that we *can* say (1) in HoTT,
> using "Type", because we find some encoding that we're reasonably happy
> with; there's a question which I've asked myself before:
>
> Will we not destroy the advantages of deep (over shallow) embedding if
> we fall back to encodings (and thus destroy the main selling point of
> HoTT)? For me, the justification of still using deep embedding is that
> statements using encodings (e.g. "the universe is a higher category)
> might still imply statements which don't use encodings and are
> interesting. However, if we want to develop a theory of certain higher
> structures for it's own sake, then it's not so clear to me whether it's
> really better to use the HoTT-style deep embedding.
>
> Kind regards,
> Nicolai
>
>
> On 09/05/2020 21:18, Joyal, André wrote:
> > Dear Thomas,
> >
> > You wrote
> >
> > <<In my opinion the currenrly implemented type theories are essentially
> > for proving and not for computing.
> > But if you haven't mechanized PART of equational reasoning it would be
> > much much more painful than it still is.
> > But that is "only" a pragmatic issue.>>
> >
> > Type  theory has very nice features. I wish they could be preserved and
> developped further.
> > But I find it frustrating that I cant do my everyday mathematics with it.
> > For example, I cannot  say
> >
> > (1) Let X:\Delta^{op}---->Type be a simplicial type;
> > (2) Let G be a type equipped with a group structure;
> > (3) Let BG be the classifying space of a group G;
> > (4) Let Gr be the category of groups;
> > (5) Let SType be the category of simplical types.
> > (6) Let Map(X,Y) be the simplicial types of maps X--->Y
> > between two simplicial types X and Y.
> >
> > It is crucial to have (1)
> > For example, a group could be defined to
> > be a simplicial object satisfying the Segal conditions.
> > The classifying space of a group is the colimit of this simplicial
> object.
> > The category of groups can be defined to be
> > a simplicial objects satisfiying the Rezk conditions (a complete Segal
> space).
> >
> > Is there some aspects of type theory that we may give up as a price
> > for solving these problems ?
> >
> >
> > Best,
> > André
> >
> > ________________________________________
> > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
> > Sent: Saturday, May 09, 2020 2:43 PM
> > To: Joyal, André
> > Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey;
> > Subject: Re: [HoTT] Identity versus equality
> >
> > Dear Andr'e,
> >
> >> By the way, if type theory is not very effective in practice, why do we
> insist that it should always compute?
> >> The dream of a formal system in which every proof leads to an actual
> computation may be far off.
> >> Not that we should abandon it, new discoveries are always possible.
> >> Is there a version of type theory for proving and verifying, less
> >> for computing?
> > In my opinion the currenrly implemented type theories are essentially
> > for proving and not for computing.
> > But if you haven't mechanized PART of equational reasoning it would be
> > much much more painful than it still is.
> > But that is "only" a pragmatic issue.
> >
> >> The notations of type theory are very useful in homotopy theory.
> >> But the absence of simplicial types is a serious obstacle to
> applications.
> > In cubical type theory they sort of live well with cubes not being
> > fibrant... They have them as pretypes. But maybe I misunderstand...
> >
> > Thomas
> >
>
>

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

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

* Re: [HoTT] Identity versus equality
2020-05-10 14:01                                        Michael Shulman
2020-05-10 14:20                                          Nicolai Kraus
@ 2020-05-10 19:20                                          Thorsten Altenkirch
1 sibling, 0 replies; 61+ messages in thread
From: Thorsten Altenkirch @ 2020-05-10 19:20 UTC (permalink / raw)
To: Michael Shulman
Cc: Jon Sterling, 'Martin Escardo' via Homotopy Type Theory

﻿On 10/05/2020, 15:06, "Michael Shulman" <shu...@sandiego.edu> wrote:

On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type

We can certainly *talk* about simplicial types in 2LTT as exofunctors
from the exocategory Delta to the exocategory Type.  I assume the
point you're making is that we don't have a (fibrant) *type of*
simplicial types, whereas we do have a fibrant type of semisimplicial
types (under appropriate axioms)?

Yes, by talking about I meant within HoTT. I mean we want to understand them as structures not just as some set-level encoding.

Also I find the Kan-condition more natural in HoTT because we just need to state an equivalence. On the level of set-level Mathematics we either hide the witness or we need to introduce uniformity conditions.

I also don't think it is an issue that Delta is not direct because Delta is based on the hack to build identities into the framework but obtain composition via the Kan condition. Hence I think we should represent identities in the same way as composition.

> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.

Personally, I think the best axiom to use here is that exo-Nat is
*cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy.  We
don't know how to model "exo-Nat is fibrant" in all higher toposes,
but it's easy to interpret "exo-Nat is cofibrant" in such models,
since Pi-types with domain exo-Nat are just externally-infinite
products.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
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] 61+ messages in thread

* Re: [HoTT] Identity versus equality
2020-05-10 19:18                                      Nicolai Kraus
@ 2020-05-10 20:22                                        Michael Shulman
2020-05-10 22:08                                          Joyal, André
From: Michael Shulman @ 2020-05-10 20:22 UTC (permalink / raw)
To: Nicolai Kraus
Cc: Joyal, André,
Thomas Streicher, David Roberts, Thorsten Altenkirch,

I'm not sure I understand the meanings of "deep" and "shallow"
completely, but the dichotomy seems similar to what we sometimes call
"analytic" and "synthetic".  Any foundational theory only
directly/synthetically represents a few concepts; all others have to
be encoded into it "analytically".  In ZFC, the synthetic objects are
well-founded membership structures; in ETCS the synthetic objects are
featureless point-sets and functions; in HoTT the synthetic objects
are oo-groupoids.

It seems reasonable to me to argue that whenever we use the
fundamental objects of the framework we should treat them
synthetically, but not expect any other structures to be synthetic.
When working in ZFC, it would be perverse to constantly work with
well-founded membership structures rather than simply use sets.  And
when working in HoTT, it would be perverse to work with oo-groupoids
defined in terms of set rather than simply use types.  But neither ZFC
nor HoTT has a synthetic notion of "simplicial oo-groupoid" or
"oo-category", so in both cases those structures have to be defined
analytically -- the only difference is that the oo-groupoid
"ingredients" are in ZFC themselves analytic whereas in HoTT those
ingredients are synthetic.

On Sun, May 10, 2020 at 12:18 PM Nicolai Kraus <nicola...@gmail.com> wrote:
>
> In the last paragraph of my message below, the words "deep" and "shallow" have to be swapped.
>
> On Sun, May 10, 2020 at 5:51 PM Nicolai Kraus <nicola...@gmail.com> wrote:
>>
>> Dear André and everyone,
>>
>> I feel it's worth pointing out that there are two strategies to express
>> "everyday mathematics" in HoTT. In CS-speak, they would probably be
>> called "shallow embedding" and "deep embedding". Shallow embedding is
>> the "HoTT style", deep embedding is the "pre-HoTT type theory style".
>> Shallow means that one uses that the host language shares structure with
>> the object one wants to define, while deep means one doesn't. To explain
>> what I mean, let's look at the type theoretic definition of a group (a
>> 1-group, not a higher group).
>>
>> Definition using deep embedding: A group is a tuple
>> (X,h,e,o,i,assoc,...), where
>>    X : Type     -- carrier
>>    h : is-0-truncated(X)     -- carrier is set
>>    e : X   -- unit
>>    o : X * X -> X     -- composition
>>    i : X -> X     -- inverses
>>    assoc : (h o g) o f = h o (g o f)
>>    ... [and so on]
>>
>> Definition using shallow embedding: A group is a pointed connected 1-type.
>>
>> Fortunately, these definitions are equivalent (via the Eilenberg-McLan
>> spaces construction). But they behave differently when we want to work
>> with them or change them. It's easy to change the second definition to
>> define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 ,
>> arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there
>> is a nice way for the first definition. The second definition has better
>> computational properties than the first.
>>
>> When you say this:
>>
>>  > But I find it frustrating that I cant do my everyday mathematics with it.
>>  > For example, I cannot  say
>>  >
>>  > (1) Let X:\Delta^{op}---->Type be a simplicial type;
>>
>> You are referring to shallow embedding. In everyday mathematics, you
>> don't say (1) either. You probably say (1) with "Type" replaced by "Set"
>> or by "simplicial set". Both of these can be expressed straightforwardly
>> in type theory using only (h-)sets (i.e. embedding deeply).
>>
>> We strive to use shallow embedding as often as possible for the reasons
>> in the above example. But let's assume that we *can* say (1) in HoTT,
>> using "Type", because we find some encoding that we're reasonably happy
>> with; there's a question which I've asked myself before:
>>
>> Will we not destroy the advantages of deep (over shallow) embedding if
>> we fall back to encodings (and thus destroy the main selling point of
>> HoTT)? For me, the justification of still using deep embedding is that
>> statements using encodings (e.g. "the universe is a higher category)
>> might still imply statements which don't use encodings and are
>> interesting. However, if we want to develop a theory of certain higher
>> structures for it's own sake, then it's not so clear to me whether it's
>> really better to use the HoTT-style deep embedding.
>>
>> Kind regards,
>> Nicolai
>>
>>
>> On 09/05/2020 21:18, Joyal, André wrote:
>> > Dear Thomas,
>> >
>> > You wrote
>> >
>> > <<In my opinion the currenrly implemented type theories are essentially
>> > for proving and not for computing.
>> > But if you haven't mechanized PART of equational reasoning it would be
>> > much much more painful than it still is.
>> > But that is "only" a pragmatic issue.>>
>> >
>> > Type  theory has very nice features. I wish they could be preserved and developped further.
>> > But I find it frustrating that I cant do my everyday mathematics with it.
>> > For example, I cannot  say
>> >
>> > (1) Let X:\Delta^{op}---->Type be a simplicial type;
>> > (2) Let G be a type equipped with a group structure;
>> > (3) Let BG be the classifying space of a group G;
>> > (4) Let Gr be the category of groups;
>> > (5) Let SType be the category of simplical types.
>> > (6) Let Map(X,Y) be the simplicial types of maps X--->Y
>> > between two simplicial types X and Y.
>> >
>> > It is crucial to have (1)
>> > For example, a group could be defined to
>> > be a simplicial object satisfying the Segal conditions.
>> > The classifying space of a group is the colimit of this simplicial object.
>> > The category of groups can be defined to be
>> > a simplicial objects satisfiying the Rezk conditions (a complete Segal space).
>> >
>> > Is there some aspects of type theory that we may give up as a price
>> > for solving these problems ?
>> >
>> >
>> > Best,
>> > André
>> >
>> > ________________________________________
>> > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
>> > Sent: Saturday, May 09, 2020 2:43 PM
>> > To: Joyal, André
>> > Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
>> > Subject: Re: [HoTT] Identity versus equality
>> >
>> > Dear Andr'e,
>> >
>> >> By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
>> >> The dream of a formal system in which every proof leads to an actual computation may be far off.
>> >> Not that we should abandon it, new discoveries are always possible.
>> >> Is there a version of type theory for proving and verifying, less
>> >> for computing?
>> > In my opinion the currenrly implemented type theories are essentially
>> > for proving and not for computing.
>> > But if you haven't mechanized PART of equational reasoning it would be
>> > much much more painful than it still is.
>> > But that is "only" a pragmatic issue.
>> >
>> >> The notations of type theory are very useful in homotopy theory.
>> >> But the absence of simplicial types is a serious obstacle to applications.
>> > In cubical type theory they sort of live well with cubes not being
>> > fibrant... They have them as pretypes. But maybe I misunderstand...
>> >
>> > Thomas
>> >
>>

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

* RE: [HoTT] Identity versus equality
2020-05-10 20:22                                        Michael Shulman
@ 2020-05-10 22:08                                          Joyal, André
0 siblings, 0 replies; 61+ messages in thread
From: Joyal, André @ 2020-05-10 22:08 UTC (permalink / raw)
To: Michael Shulman, Nicolai Kraus
Cc: Thomas Streicher, David Roberts, Thorsten Altenkirch,

Unfortunately, I must take a break from the present discussion.
I would like to thank David, Jon, Micheal, Nicolai, Steve, Thomas, Thorsten and Ulrik
for expressing their view on the problems raised.
I feel confident that we are collectively moving toward one or many solutiona.

Best,
André

________________________________________
From: Michael Shulman [shu...@sandiego.edu]
Sent: Sunday, May 10, 2020 4:22 PM
To: Nicolai Kraus
Cc: Joyal, André; Thomas Streicher; David Roberts; Thorsten Altenkirch; Steve Awodey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

I'm not sure I understand the meanings of "deep" and "shallow"
completely, but the dichotomy seems similar to what we sometimes call
"analytic" and "synthetic".  Any foundational theory only
directly/synthetically represents a few concepts; all others have to
be encoded into it "analytically".  In ZFC, the synthetic objects are
well-founded membership structures; in ETCS the synthetic objects are
featureless point-sets and functions; in HoTT the synthetic objects
are oo-groupoids.

It seems reasonable to me to argue that whenever we use the
fundamental objects of the framework we should treat them
synthetically, but not expect any other structures to be synthetic.
When working in ZFC, it would be perverse to constantly work with
well-founded membership structures rather than simply use sets.  And
when working in HoTT, it would be perverse to work with oo-groupoids
defined in terms of set rather than simply use types.  But neither ZFC
nor HoTT has a synthetic notion of "simplicial oo-groupoid" or
"oo-category", so in both cases those structures have to be defined
analytically -- the only difference is that the oo-groupoid
"ingredients" are in ZFC themselves analytic whereas in HoTT those
ingredients are synthetic.

On Sun, May 10, 2020 at 12:18 PM Nicolai Kraus <nicola...@gmail.com> wrote:
>
> In the last paragraph of my message below, the words "deep" and "shallow" have to be swapped.
>
> On Sun, May 10, 2020 at 5:51 PM Nicolai Kraus <nicola...@gmail.com> wrote:
>>
>> Dear André and everyone,
>>
>> I feel it's worth pointing out that there are two strategies to express
>> "everyday mathematics" in HoTT. In CS-speak, they would probably be
>> called "shallow embedding" and "deep embedding". Shallow embedding is
>> the "HoTT style", deep embedding is the "pre-HoTT type theory style".
>> Shallow means that one uses that the host language shares structure with
>> the object one wants to define, while deep means one doesn't. To explain
>> what I mean, let's look at the type theoretic definition of a group (a
>> 1-group, not a higher group).
>>
>> Definition using deep embedding: A group is a tuple
>> (X,h,e,o,i,assoc,...), where
>>    X : Type     -- carrier
>>    h : is-0-truncated(X)     -- carrier is set
>>    e : X   -- unit
>>    o : X * X -> X     -- composition
>>    i : X -> X     -- inverses
>>    assoc : (h o g) o f = h o (g o f)
>>    ... [and so on]
>>
>> Definition using shallow embedding: A group is a pointed connected 1-type.
>>
>> Fortunately, these definitions are equivalent (via the Eilenberg-McLan
>> spaces construction). But they behave differently when we want to work
>> with them or change them. It's easy to change the second definition to
>> define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 ,
>> arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there
>> is a nice way for the first definition. The second definition has better
>> computational properties than the first.
>>
>> When you say this:
>>
>>  > But I find it frustrating that I cant do my everyday mathematics with it.
>>  > For example, I cannot  say
>>  >
>>  > (1) Let X:\Delta^{op}---->Type be a simplicial type;
>>
>> You are referring to shallow embedding. In everyday mathematics, you
>> don't say (1) either. You probably say (1) with "Type" replaced by "Set"
>> or by "simplicial set". Both of these can be expressed straightforwardly
>> in type theory using only (h-)sets (i.e. embedding deeply).
>>
>> We strive to use shallow embedding as often as possible for the reasons
>> in the above example. But let's assume that we *can* say (1) in HoTT,
>> using "Type", because we find some encoding that we're reasonably happy
>> with; there's a question which I've asked myself before:
>>
>> Will we not destroy the advantages of deep (over shallow) embedding if
>> we fall back to encodings (and thus destroy the main selling point of
>> HoTT)? For me, the justification of still using deep embedding is that
>> statements using encodings (e.g. "the universe is a higher category)
>> might still imply statements which don't use encodings and are
>> interesting. However, if we want to develop a theory of certain higher
>> structures for it's own sake, then it's not so clear to me whether it's
>> really better to use the HoTT-style deep embedding.
>>
>> Kind regards,
>> Nicolai
>>
>>
>> On 09/05/2020 21:18, Joyal, André wrote:
>> > Dear Thomas,
>> >
>> > You wrote
>> >
>> > <<In my opinion the currenrly implemented type theories are essentially
>> > for proving and not for computing.
>> > But if you haven't mechanized PART of equational reasoning it would be
>> > much much more painful than it still is.
>> > But that is "only" a pragmatic issue.>>
>> >
>> > Type  theory has very nice features. I wish they could be preserved and developped further.
>> > But I find it frustrating that I cant do my everyday mathematics with it.
>> > For example, I cannot  say
>> >
>> > (1) Let X:\Delta^{op}---->Type be a simplicial type;
>> > (2) Let G be a type equipped with a group structure;
>> > (3) Let BG be the classifying space of a group G;
>> > (4) Let Gr be the category of groups;
>> > (5) Let SType be the category of simplical types.
>> > (6) Let Map(X,Y) be the simplicial types of maps X--->Y
>> > between two simplicial types X and Y.
>> >
>> > It is crucial to have (1)
>> > For example, a group could be defined to
>> > be a simplicial object satisfying the Segal conditions.
>> > The classifying space of a group is the colimit of this simplicial object.
>> > The category of groups can be defined to be
>> > a simplicial objects satisfiying the Rezk conditions (a complete Segal space).
>> >
>> > Is there some aspects of type theory that we may give up as a price
>> > for solving these problems ?
>> >
>> >
>> > Best,
>> > André
>> >
>> > ________________________________________
>> > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
>> > Sent: Saturday, May 09, 2020 2:43 PM
>> > To: Joyal, André
>> > Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
>> > Subject: Re: [HoTT] Identity versus equality
>> >
>> > Dear Andr'e,
>> >
>> >> By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
>> >> The dream of a formal system in which every proof leads to an actual computation may be far off.
>> >> Not that we should abandon it, new discoveries are always possible.
>> >> Is there a version of type theory for proving and verifying, less
>> >> for computing?
>> > In my opinion the currenrly implemented type theories are essentially
>> > for proving and not for computing.
>> > But if you haven't mechanized PART of equational reasoning it would be
>> > much much more painful than it still is.
>> > But that is "only" a pragmatic issue.
>> >
>> >> The notations of type theory are very useful in homotopy theory.
>> >> But the absence of simplicial types is a serious obstacle to applications.
>> > In cubical type theory they sort of live well with cubes not being
>> > fibrant... They have them as pretypes. But maybe I misunderstand...
>> >
>> > Thomas
>> >
>>

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

* Re: [HoTT] Identity versus equality
2020-05-10 18:04                                      Joyal, André
@ 2020-05-11  7:33                                        Thomas Streicher
2020-05-11 14:54                                          Joyal, André
From: Thomas Streicher @ 2020-05-11  7:33 UTC (permalink / raw)
To: Joyal, André; +Cc: Ulrik Buchholtz, Homotopy Type Theory

Dear Andr"e,

the exo/endo distinction is different from external/internal. It is like
L in set theory ZF which does not allow one to prove consisteny of ZF.
(An aside: why do internal cats play such an important role in traditional
topos theory and are evil in Hott?)

Thomas

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

* RE: [HoTT] Identity versus equality
2020-05-11  7:33                                        Thomas Streicher
@ 2020-05-11 14:54                                          Joyal, André
2020-05-11 16:37                                            stre...
From: Joyal, André @ 2020-05-11 14:54 UTC (permalink / raw)
To: Thomas Streicher; +Cc: Ulrik Buchholtz, Homotopy Type Theory

Thank you for pointing out the case of the universe of constructible sets L.
It is internal to ZF because it is was constructed from ordinals in ZF.
Could it be also external to ZF ?
Gödel thought that ordinals and sets are real, like matter, but of a different kind.
He was the first to use the full power of mathematics for studying formal logic.
Most logicians believe that natural numbers are real.
They use natural numbers and induction for studying formal systems.

Best,
André

PS: It is not easy to stop participating to this interesting discussion!

________________________________________
Sent: Monday, May 11, 2020 3:33 AM
To: Joyal, André
Cc: Ulrik Buchholtz; Homotopy Type Theory
Subject: Re: [HoTT] Identity versus equality

Dear Andr"e,

the exo/endo distinction is different from external/internal. It is like
L in set theory ZF which does not allow one to prove consisteny of ZF.
(An aside: why do internal cats play such an important role in traditional
topos theory and are evil in Hott?)

Thomas

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

* RE: [HoTT] Identity versus equality
2020-05-11 14:54                                          Joyal, André
@ 2020-05-11 16:37                                            stre...
2020-05-11 16:42                                              Michael Shulman
From: stre... @ 2020-05-11 16:37 UTC (permalink / raw)
To: "Joyal, André"
Cc: Thomas Streicher, Ulrik Buchholtz, Homotopy Type Theory

> Thank you for pointing out the case of the universe of constructible sets
> L.
> It is internal to ZF because it is was constructed from ordinals in ZF.
> Could it be also external to ZF ?

Anything internal can be externalized but not the other way round.

The point I tried to make was that in the usual models of 2-level type
theory the homotopical part is not internal to the ambient nonhomotopical
part.

> GÃ¶del thought that ordinals and sets are real, like matter, but of a
> different kind.
> He was the first to use the full power of mathematics for studying formal
> logic.
> Most logicians believe that natural numbers are real.
> They use natural numbers and induction for studying formal systems.

Indeed, Goedel was the first one who took serious the difference between
syntax and semantics. This was crucial for his findings.
That he nevertheless was a dyed in the wool Platonist was a bit inconsequent
but nobody is perfect :-)

Thomas

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

* Re: [HoTT] Identity versus equality
2020-05-11 16:37                                            stre...
@ 2020-05-11 16:42                                              Michael Shulman
2020-05-11 17:27                                                Thomas Streicher
From: Michael Shulman @ 2020-05-11 16:42 UTC (permalink / raw)
To: Thomas Streicher; +Cc: Homotopy Type Theory

FWIW there is no trouble at all with "internal categories" in HoTT;
they just correspond to (pre)categories in the smallest universe.
Some of them will naturally be univalent categories, while others will
naturally be strict categories.  If we want to "do category theory"
with the latter we can Rezk-complete them to univalent ones, but
sometimes this is unnecessary, e.g. if our goal is to talk about
"internal presheaves" on them then these are just contravariant
functors to the (univalent) category Set, and the universal property
of Rezk-completion says that it doesn't matter whether or not we
Rezk-complete the domain before talking about presheaves.  In
categories internally we are externally talking about *stacks*, with
the "weak equivalences" automatically inverted (but if for some reason
we don't want to do that, we can stick with strict categories).

On Mon, May 11, 2020 at 9:37 AM <stre...@mathematik.tu-darmstadt.de> wrote:
>
> > Thank you for pointing out the case of the universe of constructible sets
> > L.
> > It is internal to ZF because it is was constructed from ordinals in ZF.
> > Could it be also external to ZF ?
>
> Anything internal can be externalized but not the other way round.
>
> The point I tried to make was that in the usual models of 2-level type
> theory the homotopical part is not internal to the ambient nonhomotopical
> part.
>
> > Gödel thought that ordinals and sets are real, like matter, but of a
> > different kind.
> > He was the first to use the full power of mathematics for studying formal
> > logic.
> > Most logicians believe that natural numbers are real.
> > They use natural numbers and induction for studying formal systems.
>
> Indeed, Goedel was the first one who took serious the difference between
> syntax and semantics. This was crucial for his findings.
> That he nevertheless was a dyed in the wool Platonist was a bit inconsequent
> but nobody is perfect :-)
>
> 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.

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

* Re: [HoTT] Identity versus equality
2020-05-11 16:42                                              Michael Shulman
@ 2020-05-11 17:27                                                Thomas Streicher
0 siblings, 0 replies; 61+ messages in thread
From: Thomas Streicher @ 2020-05-11 17:27 UTC (permalink / raw)
To: Michael Shulman; +Cc: Homotopy Type Theory

> FWIW there is no trouble at all with "internal categories" in HoTT;

what I meant is that they are "evil" in the sense that they allow one
to speak about equality of objects
but if you do it in the simplicial sets model of HoTT then they are not quite
the same as categories internal to sSet
they are rather the unstraightenings of simplicially enriched cats
whose homobjects are all contractible

the contractible objects in sSet are much richer than the subobjects of 1

one should not forget that the logic of sSet when viewed at
homotopically is boolean whereas the traditional logic of sSet is not
at all

but I do understand that ordinary finite limit cats do live in sSet
via nerve

Thomas

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

end of thread, other threads:[~2020-05-11 17:27 UTC | newest]

2020-05-05  8:47 Identity versus equality Ansten Mørch Klev
2020-05-06 16:02  [HoTT] " Joyal, André
2020-05-06 19:01    Steve Awodey
2020-05-06 19:18      Michael Shulman
2020-05-06 19:31        Steve Awodey
2020-05-06 20:30          Joyal, André
2020-05-06 22:52          Thorsten Altenkirch
2020-05-06 22:54        Thorsten Altenkirch
2020-05-06 23:29          Joyal, André
2020-05-07  6:11            Egbert Rijke
2020-05-07  6:58            Thorsten Altenkirch
2020-05-07  9:04              Ansten Mørch Klev
2020-05-07 10:09              Thomas Streicher
2020-05-07 16:13                Joyal, André
2020-05-07 21:41                  David Roberts
2020-05-07 23:43                    Joyal, André
2020-05-07 23:56                      David Roberts
2020-05-08  6:40                        Thomas Streicher
2020-05-08 21:06                          Joyal, André
2020-05-08 23:44                            Steve Awodey
2020-05-09  2:46                              Joyal, André
2020-05-09  3:09                                Jon Sterling
2020-05-09  2:50                                Steve Awodey
2020-05-09  8:28                            Thomas Streicher
2020-05-09 15:53                              Joyal, André
2020-05-09 18:43                                Thomas Streicher
2020-05-09 20:18                                  Joyal, André
2020-05-09 21:27                                    Jon Sterling
2020-05-10  2:19                                      Joyal, André
2020-05-10  3:04                                        Jon Sterling
2020-05-10  9:09                                          Thomas Streicher
2020-05-10 11:59                                            Thorsten Altenkirch
2020-05-10 11:46                                      Thorsten Altenkirch
2020-05-10 14:01                                        Michael Shulman
2020-05-10 14:20                                          Nicolai Kraus
2020-05-10 14:34                                            Michael Shulman
2020-05-10 14:52                                              Nicolai Kraus
2020-05-10 15:16                                                Michael Shulman
2020-05-10 15:23                                                  Nicolai Kraus
2020-05-10 16:13                                                    Nicolai Kraus
2020-05-10 16:28                                                      Michael Shulman
2020-05-10 18:18                                                        Nicolai Kraus
2020-05-10 19:15                                              Thorsten Altenkirch
2020-05-10 19:20                                          Thorsten Altenkirch
2020-05-10 12:53                                    Ulrik Buchholtz
2020-05-10 14:01                                      Michael Shulman
2020-05-10 14:27                                        Nicolai Kraus
2020-05-10 15:35                                          Ulrik Buchholtz
2020-05-10 16:30                                            Michael Shulman
2020-05-10 18:56                                            Nicolai Kraus
2020-05-10 18:04                                      Joyal, André
2020-05-11  7:33                                        Thomas Streicher
2020-05-11 14:54                                          Joyal, André
2020-05-11 16:37                                            stre...
2020-05-11 16:42                                              Michael Shulman
2020-05-11 17:27                                                Thomas Streicher
2020-05-10 16:51                                    Nicolai Kraus
2020-05-10 18:57                                      Michael Shulman
2020-05-10 19:18                                      Nicolai Kraus
2020-05-10 20:22                                        Michael Shulman
2020-05-10 22:08                                          Joyal, André


This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).