[-- 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' 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! [-- Attachment #2: Type: text/html, Size: 2519 bytes --]

[-- 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. 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é ________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [anste...@gmail.com] Sent: Tuesday, May 05, 2020 4:47 AM To: HomotopyT...@googlegroups.com 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>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%40mail.gmail.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%40mail.gmail.com?utm_medium=email&utm_source=footer>. [-- Attachment #2: Type: text/html, Size: 5657 bytes --]

[-- 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é > From: homotopyt...@googlegroups.com <mailto:homotopyt...@googlegroups.com> [homotopyt...@googlegroups.com <mailto:homotopyt...@googlegroups.com>] on behalf of Ansten Mørch Klev [anste...@gmail.com <mailto:anste...@gmail.com>] > Sent: Tuesday, May 05, 2020 4:47 AM > To: HomotopyT...@googlegroups.com <mailto:HomotopyT...@googlegroups.com> > 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>. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%40mail.gmail.com <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%40mail.gmail.com?utm_medium=email&utm_source=footer>. > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyT...@googlegroups.com <mailto:HomotopyT...@googlegroups.com>. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca <https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca?utm_medium=email&utm_source=footer>. [-- Attachment #2: Type: text/html, Size: 15035 bytes --]

```
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é
> ________________________________
> From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [anste...@gmail.com]
> Sent: Tuesday, May 05, 2020 4:47 AM
> To: HomotopyT...@googlegroups.com
> 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.
```

```
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é
>> ________________________________
>> From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [anste...@gmail.com]
>> Sent: Tuesday, May 05, 2020 4:47 AM
>> To: HomotopyT...@googlegroups.com
>> 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.
```

```
Dear Steve and Mike,
Thank you for your reply.
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
Cc: Joyal, André; HomotopyT...@googlegroups.com
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é
>> ________________________________
>> From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [anste...@gmail.com]
>> Sent: Tuesday, May 05, 2020 4:47 AM
>> To: HomotopyT...@googlegroups.com
>> 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.
```

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é >> ________________________________ >> From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [anste...@gmail.com] >> Sent: Tuesday, May 05, 2020 4:47 AM >> To: HomotopyT...@googlegroups.com >> 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 message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

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é > ________________________________ > From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [anste...@gmail.com] > Sent: Tuesday, May 05, 2020 4:47 AM > To: HomotopyT...@googlegroups.com > 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 message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

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 Cc: Joyal, André; homotopyt...@googlegroups.com 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é > ________________________________ > From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [anste...@gmail.com] > Sent: Tuesday, May 05, 2020 4:47 AM > To: HomotopyT...@googlegroups.com > 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 message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

[-- Attachment #1: 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 > Cc: Joyal, André; homotopyt...@googlegroups.com > 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é > > ________________________________ > > From: homotopyt...@googlegroups.com [ > homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [ > anste...@gmail.com] > > Sent: Tuesday, May 05, 2020 4:47 AM > > To: HomotopyT...@googlegroups.com > > 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 > message in error, please contact the sender and delete the email and > attachment. > > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored > where permitted by law. > > > > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyT...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F526C%40Pli.gst.uqam.ca > . > [-- Attachment #2: Type: text/html, Size: 16178 bytes --]

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 Cc: Joyal, André; homotopyt...@googlegroups.com 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é > ________________________________ > From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [anste...@gmail.com] > Sent: Tuesday, May 05, 2020 4:47 AM > To: HomotopyT...@googlegroups.com > 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 message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

[-- Attachment #1: 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, > > 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 > Cc: Joyal, André; homotopyt...@googlegroups.com > 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é > > ________________________________ > > From: homotopyt...@googlegroups.com [ > homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [ > anste...@gmail.com] > > Sent: Tuesday, May 05, 2020 4:47 AM > > To: HomotopyT...@googlegroups.com > > 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 > message in error, please contact the sender and delete the email and > attachment. > > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored > where permitted by law. > > > > > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment. > > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored > where permitted by law. > > > > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyT...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9%40nottingham.ac.uk > . > [-- Attachment #2: Type: text/html, Size: 19093 bytes --]

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

Thank you all for your comments. 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é ________________________________________ From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] 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

[-- 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: > Thank you all for your comments. > > 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é > > > > ________________________________________ > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] > 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 > > > > -- > 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/8C57894C7413F04A98DDF5629FEC90B1652F5334%40Pli.gst.uqam.ca > . > [-- Attachment #2: Type: text/html, Size: 7722 bytes --]

[-- 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: Thank you all for your comments. 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é ________________________________________ From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de<mailto:stre...@mathematik.tu-darmstadt.de>] Sent: Thursday, May 07, 2020 6:09 AM To: Thorsten Altenkirch Cc: Joyal, André; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com<mailto: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 -- 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 --]

[-- 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 > 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> wrote: > >> Thank you all for your comments. >> >> 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é >> >> >> >> ________________________________________ >> From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] >> 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 >> >> >> >> -- >> 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/8C57894C7413F04A98DDF5629FEC90B1652F5334%40Pli.gst.uqam.ca >> . >> > [-- Attachment #2: Type: text/html, Size: 11466 bytes --]

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 sad about working in a framework not allowing to speak about them.) 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 adherents of the "multiverse" view of set theory would share this view! 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!

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 sad about working in a framework not allowing to speak about them.) 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 adherents of the "multiverse" view of set theory would share this view! 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!

```
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
> 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
> sad about working in a framework not allowing to speak about them.)
> 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
> adherents of the "multiverse" view of set theory would share this view!
> 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.
```

```
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
> 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
> sad about working in a framework not allowing to speak about them.)
> 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
> adherents of the "multiverse" view of set theory would share this view!
> 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.
```

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

```
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
> 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
> > 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
> > sad about working in a framework not allowing to speak about them.)
> > 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
> > adherents of the "multiverse" view of set theory would share this view!
> > 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
> an email to HomotopyT...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F5565%40Pli.gst.uqam.ca.
>
```

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

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é ________________________________________ From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] 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

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

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

```
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é
>
> ________________________________________
> 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
>
> --
> 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/8C57894C7413F04A98DDF5629FEC90B1652F563A%40Pli.gst.uqam.ca.
>
```

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é ________________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Jon Sterling [j...@jonmsterling.com] 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é > > ________________________________________ > 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 > > -- > 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/8C57894C7413F04A98DDF5629FEC90B1652F563A%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/b1d32ac0-e364-4405-9e48-e0e1e0b37732%40www.fastmail.com.

```
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é
>
> ________________________________________
> From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Jon Sterling [j...@jonmsterling.com]
> 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é
>>
>> ________________________________________
>> 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
>>
>> --
>> 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/8C57894C7413F04A98DDF5629FEC90B1652F563A%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/b1d32ac0-e364-4405-9e48-e0e1e0b37732%40www.fastmail.com.
```

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 still nowadays) traditional logicians are mainly adherents of a one 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

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) Similarly we can add degeneracies (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é > > ________________________________________ > 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 > > -- > 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/8C57894C7413F04A98DDF5629FEC90B1652F563A%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/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 message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

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 message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

[-- Attachment #1.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 --]

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!

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.

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

```
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 #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 --]

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

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

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

[-- 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 > >>>> "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 > . > > [-- Attachment #2: Type: text/html, Size: 6339 bytes --]

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

```
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.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/7b9eb7c9-040a-46e8-b470-28958f8d7713%40googlegroups.com.
```

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

[-- 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é ________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ulrik Buchholtz [ulrikbu...@gmail.com] 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? 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 -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyT...@googlegroups.com<mailto:HomotopyT...@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/e47e6263-d0eb-4882-ab07-e31483095bd4%40googlegroups.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/e47e6263-d0eb-4882-ab07-e31483095bd4%40googlegroups.com?utm_medium=email&utm_source=footer>. [-- Attachment #2: Type: text/html, Size: 8945 bytes --]

[-- 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 > 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 > . > > -- > 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/CAOvivQz_JCE8QPTomY7ViOX%3DPgzZ_5aM3t9fx613jyfuOAUtvA%40mail.gmail.com > . > [-- Attachment #2: Type: text/html, Size: 8873 bytes --]

[-- 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 instead, as e.g. in https://arxiv.org/abs/2004.06572 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 > email to HomotopyT...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/7b9eb7c9-040a-46e8-b470-28958f8d7713%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/7b9eb7c9-040a-46e8-b470-28958f8d7713%40googlegroups.com?utm_medium=email&utm_source=footer> > . > [-- Attachment #2: Type: text/html, Size: 5003 bytes --]

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

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 > "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 This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

[-- Attachment #1: 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; > 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 > > > > [-- Attachment #2: Type: text/html, Size: 7081 bytes --]

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 message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

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

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

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

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! ________________________________________ From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] 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

> 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

```
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
addition, we get the bonus that when talking about univalent
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.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/0388695a1dfc717f9c5e458937dff760.squirrel%40webmail.mathematik.tu-darmstadt.de.
```

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