[-- Attachment #1.1: Type: text/plain, Size: 3184 bytes --] Hello, HoTT community. I've learned a bit about HoTT in bits of spare time over the past few years, and have come up with some questions I can't answer on my own. It was suggested that I ask them on this list. I will start with a few small questions, and if anyone in the community here has time to answer them, then I'll continue with others as needed. Thank you in advance for any help you can give. (Where I'm coming from: I'm a mathematician; my dissertation was on intermediate logics, but I haven't focused on logic much for the past 15 years, instead doing mathematical software and some applied mathematics. I have a passion for clear exposition, so as I learn about HoTT, I process it by writing detailed notes to myself, explaining it as clearly as I can. When I can't explain something clearly, I flag it as a question. I'm bringing those questions here.) Here are three to start. 1. Very early in the HoTT book, it talks about the difference between types and sets, and says that HoTT encourages us to see sets as spaces. Yet in a set of lecture videos Robert Harper did that I watched on YouTube (which also seem to have disappeared, so I cannot link to them here), he said that Extensional Type Theory takes Intuitionistic Type Theory in a different direction than HoTT does, formalizing the idea that types are sets. Why does the HoTT book not mention this possibility? Why does ETT not seem to get as much press as HoTT? 2. When that same text introduces judgmental equality, it claims that it is a decidable relation. It does not seem to prove this, and so I suspected that perhaps the evidence was in Appendix A, where things are done more formally (twice, even). The first of these two formalisms places some restrictions on how one can introduce new judgmental equalities, which seem sufficient to guarantee its decidability, but at no point is an algorithm for deciding it given. Is the algorithm simply to apply the only applicable rule over and over to reduce each side, and then compare for exact syntactic equality? 3. One of my favorite things about HoTT as a foundation for mathematics actually comes just from DTT: Once you've formalized pi types, you can define all of logic and (lots of) mathematics. But then the hierarchy of type universes seem to require that we understand the natural numbers, which is way more complicated than just pi types, and thus highly disappointing to have to bring in at a foundational level. Am I right to be disappointed about that or am I missing something? Thanks in advance for any help you have time and interest to provide! Nathan Carter -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3666 bytes --] <div dir="ltr"><div><br></div><div>Hello, HoTT community.</div><div><br></div><div>I've learned a bit about HoTT in bits of spare time over the past few years, and have come up with some questions I can't answer on my own. It was suggested that I ask them on this list. I will start with a few small questions, and if anyone in the community here has time to answer them, then I'll continue with others as needed. Thank you in advance for any help you can give.</div><div><br></div><div>(Where I'm coming from: I'm a mathematician; my dissertation was on intermediate logics, but I haven't focused on logic much for the past 15 years, instead doing mathematical software and some applied mathematics. I have a passion for clear exposition, so as I learn about HoTT, I process it by writing detailed notes to myself, explaining it as clearly as I can. When I can't explain something clearly, I flag it as a question. I'm bringing those questions here.)</div><div><br></div><div>Here are three to start.</div><div><ol><li>Very early in the HoTT book, it talks about the difference between types and sets, and says that HoTT encourages us to see sets as spaces. Yet in a set of lecture videos Robert Harper did that I watched on YouTube (which also seem to have disappeared, so I cannot link to them here), he said that Extensional Type Theory takes Intuitionistic Type Theory in a different direction than HoTT does, formalizing the idea that types are sets. Why does the HoTT book not mention this possibility? Why does ETT not seem to get as much press as HoTT?</li><li>When that same text introduces judgmental equality, it claims that it is a decidable relation. It does not seem to prove this, and so I suspected that perhaps the evidence was in Appendix A, where things are done more formally (twice, even). The first of these two formalisms places some restrictions on how one can introduce new judgmental equalities, which seem sufficient to guarantee its decidability, but at no point is an algorithm for deciding it given. Is the algorithm simply to apply the only applicable rule over and over to reduce each side, and then compare for exact syntactic equality?</li><li>One of my favorite things about HoTT as a foundation for mathematics actually comes just from DTT: Once you've formalized pi types, you can define all of logic and (lots of) mathematics. But then the hierarchy of type universes seem to require that we understand the natural numbers, which is way more complicated than just pi types, and thus highly disappointing to have to bring in at a foundational level. Am I right to be disappointed about that or am I missing something?</li></ol></div><div>Thanks in advance for any help you have time and interest to provide!</div><div><br></div><div>Nathan Carter</div><div><br></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 4860 bytes --] Hi Nathan, I'm a bit rusty and don't want to say potentially misleading things on a public forum, so I'm messaging offlist. Hopefully someone else gives more thorough answers: 1. ETT provides little (if any) technical value over set theory, at the cost of more bureaucracy, so it's main draw is the philosophical underpinnings. Since it also seems to conflict with computational intuitions, it alienates not only the classical mathematician, but also the computer scientist--this leaves a small audience. 2. I believe you are correct 3. Without *any* type universes, you only get the types of System T---So you get a system that corresponds to higher-typed Heyting arithmetic. So we need at least one universe. The HoTT book doesn't *really* use the natural numbers, only successor and a (binary) least upper bound operator. I guess this corresponds roughly to Robinson's Arithmetic? Best, Cory On Thu, Jun 20, 2019 at 5:16 PM Nathan Carter <nathancarter5@gmail.com> wrote: > > Hello, HoTT community. > > I've learned a bit about HoTT in bits of spare time over the past few > years, and have come up with some questions I can't answer on my own. It > was suggested that I ask them on this list. I will start with a few small > questions, and if anyone in the community here has time to answer them, > then I'll continue with others as needed. Thank you in advance for any > help you can give. > > (Where I'm coming from: I'm a mathematician; my dissertation was on > intermediate logics, but I haven't focused on logic much for the past 15 > years, instead doing mathematical software and some applied mathematics. I > have a passion for clear exposition, so as I learn about HoTT, I process it > by writing detailed notes to myself, explaining it as clearly as I can. > When I can't explain something clearly, I flag it as a question. I'm > bringing those questions here.) > > Here are three to start. > > 1. Very early in the HoTT book, it talks about the difference between > types and sets, and says that HoTT encourages us to see sets as spaces. > Yet in a set of lecture videos Robert Harper did that I watched on YouTube > (which also seem to have disappeared, so I cannot link to them here), he > said that Extensional Type Theory takes Intuitionistic Type Theory in a > different direction than HoTT does, formalizing the idea that types are > sets. Why does the HoTT book not mention this possibility? Why does ETT > not seem to get as much press as HoTT? > 2. When that same text introduces judgmental equality, it claims that > it is a decidable relation. It does not seem to prove this, and so I > suspected that perhaps the evidence was in Appendix A, where things are > done more formally (twice, even). The first of these two formalisms places > some restrictions on how one can introduce new judgmental equalities, which > seem sufficient to guarantee its decidability, but at no point is an > algorithm for deciding it given. Is the algorithm simply to apply the only > applicable rule over and over to reduce each side, and then compare for > exact syntactic equality? > 3. One of my favorite things about HoTT as a foundation for > mathematics actually comes just from DTT: Once you've formalized pi types, > you can define all of logic and (lots of) mathematics. But then the > hierarchy of type universes seem to require that we understand the natural > numbers, which is way more complicated than just pi types, and thus highly > disappointing to have to bring in at a foundational level. Am I right to > be disappointed about that or am I missing something? > > Thanks in advance for any help you have time and interest to provide! > > Nathan Carter > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com?utm_medium=email&utm_source=footer> > . > For more options, visit https://groups.google.com/d/optout. > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADzYOhd-tHN0XO_c%2B-rW_JSU1%3DQ6CmGE3L8aSHCEW32oX%2BKttA%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 5953 bytes --] <div dir="ltr">Hi Nathan,<div><br></div><div>I'm a bit rusty and don't want to say potentially misleading things on a public forum, so I'm messaging offlist. Hopefully someone else gives more thorough answers:</div><div><br></div><div>1. ETT provides little (if any) technical value over set theory, at the cost of more bureaucracy, so it's main draw is the philosophical underpinnings. Since it also seems to conflict with computational intuitions, it alienates not only the classical mathematician, but also the computer scientist--this leaves a small audience.<br></div><div><br></div><div>2. I believe you are correct</div><div><br></div><div>3. Without *any* type universes, you only get the types of System T---So you get a system that corresponds to higher-typed Heyting arithmetic. So we need at least one universe. The HoTT book doesn't *really* use the natural numbers, only successor and a (binary) least upper bound operator. I guess this corresponds roughly to Robinson's Arithmetic?</div><div><br></div><div>Best,</div><div>Cory</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jun 20, 2019 at 5:16 PM Nathan Carter <<a href="mailto:nathancarter5@gmail.com">nathancarter5@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div><br></div><div>Hello, HoTT community.</div><div><br></div><div>I've learned a bit about HoTT in bits of spare time over the past few years, and have come up with some questions I can't answer on my own. It was suggested that I ask them on this list. I will start with a few small questions, and if anyone in the community here has time to answer them, then I'll continue with others as needed. Thank you in advance for any help you can give.</div><div><br></div><div>(Where I'm coming from: I'm a mathematician; my dissertation was on intermediate logics, but I haven't focused on logic much for the past 15 years, instead doing mathematical software and some applied mathematics. I have a passion for clear exposition, so as I learn about HoTT, I process it by writing detailed notes to myself, explaining it as clearly as I can. When I can't explain something clearly, I flag it as a question. I'm bringing those questions here.)</div><div><br></div><div>Here are three to start.</div><div><ol><li>Very early in the HoTT book, it talks about the difference between types and sets, and says that HoTT encourages us to see sets as spaces. Yet in a set of lecture videos Robert Harper did that I watched on YouTube (which also seem to have disappeared, so I cannot link to them here), he said that Extensional Type Theory takes Intuitionistic Type Theory in a different direction than HoTT does, formalizing the idea that types are sets. Why does the HoTT book not mention this possibility? Why does ETT not seem to get as much press as HoTT?</li><li>When that same text introduces judgmental equality, it claims that it is a decidable relation. It does not seem to prove this, and so I suspected that perhaps the evidence was in Appendix A, where things are done more formally (twice, even). The first of these two formalisms places some restrictions on how one can introduce new judgmental equalities, which seem sufficient to guarantee its decidability, but at no point is an algorithm for deciding it given. Is the algorithm simply to apply the only applicable rule over and over to reduce each side, and then compare for exact syntactic equality?</li><li>One of my favorite things about HoTT as a foundation for mathematics actually comes just from DTT: Once you've formalized pi types, you can define all of logic and (lots of) mathematics. But then the hierarchy of type universes seem to require that we understand the natural numbers, which is way more complicated than just pi types, and thus highly disappointing to have to bring in at a foundational level. Am I right to be disappointed about that or am I missing something?</li></ol></div><div>Thanks in advance for any help you have time and interest to provide!</div><div><br></div><div>Nathan Carter</div><div><br></div></div> <p></p> -- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com" target="_blank">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com?utm_medium=email&utm_source=footer" target="_blank">https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com</a>.<br> For more options, visit <a href="https://groups.google.com/d/optout" target="_blank">https://groups.google.com/d/optout</a>.<br> </blockquote></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CADzYOhd-tHN0XO_c%2B-rW_JSU1%3DQ6CmGE3L8aSHCEW32oX%2BKttA%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CADzYOhd-tHN0XO_c%2B-rW_JSU1%3DQ6CmGE3L8aSHCEW32oX%2BKttA%40mail.gmail.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 6304 bytes --] Hi Nathan, I can try to give answers but the answers you get may depend on the person you ask. 1. Very early in the HoTT book, it talks about the difference between types and sets, and says that HoTT encourages us to see sets as spaces. Yet in a set of lecture videos Robert Harper did that I watched on YouTube (which also seem to have disappeared, so I cannot link to them here), he said that Extensional Type Theory takes Intuitionistic Type Theory in a different direction than HoTT does, formalizing the idea that types are sets. Why does the HoTT book not mention this possibility? Why does ETT not seem to get as much press as HoTT? ETT or computational type theory relies on some notion of untyped computation which is then sorted by defining some semantic criteria for types. I prefer only to to talk about typed entities because they are the constructions which make sense and it shouldn’t be necessary to refer to some untyped codes. However, this is my preference, I am sure Bob Harper views this differently. Also the semantic definitions refer to a rather unspecified meta theory, while in a type theory specified as the initial syntax of some kind of algebras you get a precise and 1st order definition what exactly the theory and the models are. 1. When that same text introduces judgmental equality, it claims that it is a decidable relation. It does not seem to prove this, and so I suspected that perhaps the evidence was in Appendix A, where things are done more formally (twice, even). The first of these two formalisms places some restrictions on how one can introduce new judgmental equalities, which seem sufficient to guarantee its decidability, but at no point is an algorithm for deciding it given. Is the algorithm simply to apply the only applicable rule over and over to reduce each side, and then compare for exact syntactic equality? It is beyond the scope of the HoTT book to discuss the algorithm to decide definitional equality. There are a number of standard approaches to do this: you can normalize the terms in a syntactic way and use this to decide equality but then you need to prove that the normalisation procedure actually terminates and is well behaved wrt typing which isn’t trivial. Another approach is to use a constructive semantical model to normalize (this is called normalisation by evaluation) but again this isn’t completely trivial. The naïve algorithm you suggest may not take care of eta-equalities. Moreover, the theory presented in the HoTT book has a serious problem: extensionality principles like functional extensionality and univalence are added as axioms, which have no place in type theory. Their presence destroys computational adequacy, which means that a closed term of type Nat may not reduce to a numeral. Baiscally it is a programming language but we don’t know how to run the programs. This has been fixed now, by the work by Thierry Ciquand and others on cubical type theory, which uses the cubical sets interpretation of HoTT to give a constrictive semantics which in turn can be used to design a normalisation procedure which does normalize correctly, in particular it reduces closed natural numbers to numerals. There is the remaining issue that it is not known whether the cubical theory coincides with the simplicial interpretation which is the standard one in homotopy theory. 1. One of my favorite things about HoTT as a foundation for mathematics actually comes just from DTT: Once you've formalized pi types, you can define all of logic and (lots of) mathematics. But then the hierarchy of type universes seem to require that we understand the natural numbers, which is way more complicated than just pi types, and thus highly disappointing to have to bring in at a foundational level. Am I right to be disappointed about that or am I missing something? How do you do a lot of Mathematics without defining the natural numbers? The problem with the predicative hierarchy of universes is rather that it is rather clumsy in real life since everything you do is usually level polymorphic. You can sort of put this under the carpet but actual implementations of type theory haven’t yet found a good way to deal with this. Another issue with universes is that you always want more (they are like inaccessible cardinals in set theory). So for example you want to add a superuniverse which is above all the universes in the predicative hierarchy and so on. There has been some work investigating these universe hierarchies and the similarity with inaccessible cardinals is rather strong. Thorsten Thanks in advance for any help you have time and interest to provide! Nathan Carter -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com?utm_medium=email&utm_source=footer>. For more options, visit https://groups.google.com/d/optout. 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/C02F9858-5868-4447-B0C1-D1303A754F60%40exmail.nottingham.ac.uk. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 10169 bytes --] <html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"> <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8"> <meta name="Generator" content="Microsoft Word 15 (filtered medium)"> <style><!-- /* Font Definitions */ @font-face {font-family:"Cambria Math"; panose-1:2 4 5 3 5 4 6 3 2 4;} @font-face {font-family:Calibri; panose-1:2 15 5 2 2 2 4 3 2 4;} /* Style Definitions */ p.MsoNormal, li.MsoNormal, div.MsoNormal {margin:0cm; margin-bottom:.0001pt; font-size:11.0pt; font-family:"Calibri",sans-serif;} a:link, span.MsoHyperlink {mso-style-priority:99; color:blue; text-decoration:underline;} a:visited, span.MsoHyperlinkFollowed {mso-style-priority:99; color:purple; text-decoration:underline;} p.msonormal0, li.msonormal0, div.msonormal0 {mso-style-name:msonormal; mso-margin-top-alt:auto; margin-right:0cm; mso-margin-bottom-alt:auto; margin-left:0cm; font-size:11.0pt; font-family:"Calibri",sans-serif;} span.EmailStyle19 {mso-style-type:personal-reply; font-family:"Calibri",sans-serif; color:windowtext;} .MsoChpDefault {mso-style-type:export-only; font-size:10.0pt;} @page WordSection1 {size:612.0pt 792.0pt; margin:72.0pt 72.0pt 72.0pt 72.0pt;} div.WordSection1 {page:WordSection1;} /* List Definitions */ @list l0 {mso-list-id:525096075; mso-list-template-ids:1082192506;} ol {margin-bottom:0cm;} ul {margin-bottom:0cm;} --></style> </head> <body lang="EN-GB" link="blue" vlink="purple"> <div class="WordSection1"> <p class="MsoNormal">Hi Nathan,<o:p></o:p></p> <p class="MsoNormal"><o:p> </o:p></p> <p class="MsoNormal">I can try to give answers but the answers you get may depend on the person you ask.<o:p></o:p></p> <div> <div> <ol start="1" type="1"> <li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l0 level1 lfo1"> Very early in the HoTT book, it talks about the difference between types and sets, and says that HoTT encourages us to see sets as spaces. Yet in a set of lecture videos Robert Harper did that I watched on YouTube (which also seem to have disappeared, so I cannot link to them here), he said that Extensional Type Theory takes Intuitionistic Type Theory in a different direction than HoTT does, formalizing the idea that types are sets. Why does the HoTT book not mention this possibility? Why does ETT not seem to get as much press as HoTT?<o:p></o:p></li></ol> <p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">ETT or computational type theory relies on some notion of untyped computation which is then sorted by defining some semantic criteria for types. I prefer only to to talk about typed entities because they are the constructions which make sense and it shouldn’t be necessary to refer to some untyped codes. However, this is my preference, I am sure Bob Harper views this differently. Also the semantic definitions refer to a rather unspecified meta theory, while in a type theory specified as the initial syntax of some kind of algebras you get a precise and 1<sup>st</sup> order definition what exactly the theory and the models are. <o:p></o:p></p> <ol start="2" type="1"> <li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l0 level1 lfo1"> When that same text introduces judgmental equality, it claims that it is a decidable relation. It does not seem to prove this, and so I suspected that perhaps the evidence was in Appendix A, where things are done more formally (twice, even). The first of these two formalisms places some restrictions on how one can introduce new judgmental equalities, which seem sufficient to guarantee its decidability, but at no point is an algorithm for deciding it given. Is the algorithm simply to apply the only applicable rule over and over to reduce each side, and then compare for exact syntactic equality?<o:p></o:p></li></ol> <p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">It is beyond the scope of the HoTT book to discuss the algorithm to decide definitional equality. There are a number of standard approaches to do this: you can normalize the terms in a syntactic way and use this to decide equality but then you need to prove that the normalisation procedure actually terminates and is well behaved wrt typing which isn’t trivial. Another approach is to use a constructive semantical model to normalize (this is called normalisation by evaluation) but again this isn’t completely trivial. The naïve algorithm you suggest may not take care of eta-equalities.<o:p></o:p></p> <p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">Moreover, the theory presented in the HoTT book has a serious problem: extensionality principles like functional extensionality and univalence are added as axioms, which have no place in type theory. Their presence destroys computational adequacy, which means that a closed term of type Nat may not reduce to a numeral. Baiscally it is a programming language but we don’t know how to run the programs. This has been fixed now, by the work by Thierry Ciquand and others on cubical type theory, which uses the cubical sets interpretation of HoTT to give a constrictive semantics which in turn can be used to design a normalisation procedure which does normalize correctly, in particular it reduces closed natural numbers to numerals.<o:p></o:p></p> <p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">There is the remaining issue that it is not known whether the cubical theory coincides with the simplicial interpretation which is the standard one in homotopy theory.<o:p></o:p></p> <ol start="3" type="1"> <li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l0 level1 lfo1"> One of my favorite things about HoTT as a foundation for mathematics actually comes just from DTT: Once you've formalized pi types, you can define all of logic and (lots of) mathematics. But then the hierarchy of type universes seem to require that we understand the natural numbers, which is way more complicated than just pi types, and thus highly disappointing to have to bring in at a foundational level. Am I right to be disappointed about that or am I missing something?<o:p></o:p></li></ol> <p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">How do you do a lot of Mathematics without defining the natural numbers? The problem with the predicative hierarchy of universes is rather that it is rather clumsy in real life since everything you do is usually level polymorphic. You can sort of put this under the carpet but actual implementations of type theory haven’t yet found a good way to deal with this.<o:p></o:p></p> <p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">Another issue with universes is that you always want more (they are like inaccessible cardinals in set theory). So for example you want to add a superuniverse which is above all the universes in the predicative hierarchy and so on. There has been some work investigating these universe hierarchies and the similarity with inaccessible cardinals is rather strong.<o:p></o:p></p> <p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">Thorsten<o:p></o:p></p> <p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><o:p> </o:p></p> </div> <div> <p class="MsoNormal">Thanks in advance for any help you have time and interest to provide!<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal">Nathan Carter<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> </div> <p class="MsoNormal">-- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com?utm_medium=email&utm_source=footer"> https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com</a>.<br> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br> <br> <o:p></o:p></p> </div> <PRE> 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. </PRE></body> </html> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/C02F9858-5868-4447-B0C1-D1303A754F60%40exmail.nottingham.ac.uk?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/C02F9858-5868-4447-B0C1-D1303A754F60%40exmail.nottingham.ac.uk</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 6979 bytes --] 1. There are at least two ways in which types are not sets. Firstly, when reasoning classically, we have a membership relation whereby we can postulate the membership of elements in a given set. It may seem similar to a : A but in this case writing a : B would make no sense, whereas in set theory membership can be disproven. This is quite a subtle notion and is closely related to the difference between structural and material set theories which Mike Shulman wrote a nice paper on https://arxiv.org/pdf/1808.05204.pdf. But I am sure someone else here will do a better job at explain that. The second difference is what I think Harper was referring to, which is that sets are types which satisfy what is called Uniqueness of identity proofs (UIP). This means that given a : A and b : A, we can form the identity type Id(a, b). If we wish to show there is an equality between a and b we construct a term p : Id(a, b). But what if we can construct another equality q : Id(a, b)? UIP (a.k.a axiom K) ensures that there is always a term r : Id(p, q). Which in English means: Any two proofs of equality between elements of a set are themselves equal. Why does this matter? Well because in Martin-Lof type theory (with univalent universes) (the type theory that HoTT is based on), you can construct seperate proofs of the same thing. Take for example the type 2. It has two terms 1_2 : 2 and 2_2 : 2. If we consider the ways in which 2 can be equal to itself, i.e. terms of Id(2, 2), we see that (with univalence) there are two possible ways. The first is just reflexivity and the second is "an equality" which swaps 1_2 with 2_2. These are both proofs of Id(2, 2) but they are definitely not the same. And in fact can't be shown to be the same without assuming UIP. 2. One heuristic way to see that judgemental equality can be decided is by "completely computing" a given term, i.e. beta reduce it all the way down. Theorems such as Church-Rosser guarantee that the order of reductions does not matter. There are more properties such as "canonicity" which roughly state that fully reduced terms are identical. I am not an expert on these properties however but there are many experts on this list. Checking whether two terms are judgementally equal is a commonly studied problem in type theory. There are ways to test equality without fully reducing down such as the one detailed here: https://link.springer.com/chapter/10.1007/978-3-540-70594-9_4 3. Simply typed lambda calculus has "natural numbers" via the Church-encoding. The key difference between this and regular arithmetic is that you can't really define a function out of the type of such things. Or in other words, there is no recursion principle for the natural numbers. Adding such a rule would give you something like Godels system T. Universes only need a sucessor structure, and not really the full arithmetic capabilities of the natural numbers themselves. These are just some of my thoughts on your questions, hopefully it will help. Ali Caglayan On Thu, Jun 20, 2019 at 5:16 PM Nathan Carter <nathancarter5@gmail.com> wrote: > > Hello, HoTT community. > > I've learned a bit about HoTT in bits of spare time over the past few > years, and have come up with some questions I can't answer on my own. It > was suggested that I ask them on this list. I will start with a few small > questions, and if anyone in the community here has time to answer them, > then I'll continue with others as needed. Thank you in advance for any > help you can give. > > (Where I'm coming from: I'm a mathematician; my dissertation was on > intermediate logics, but I haven't focused on logic much for the past 15 > years, instead doing mathematical software and some applied mathematics. I > have a passion for clear exposition, so as I learn about HoTT, I process it > by writing detailed notes to myself, explaining it as clearly as I can. > When I can't explain something clearly, I flag it as a question. I'm > bringing those questions here.) > > Here are three to start. > > 1. Very early in the HoTT book, it talks about the difference between > types and sets, and says that HoTT encourages us to see sets as spaces. > Yet in a set of lecture videos Robert Harper did that I watched on YouTube > (which also seem to have disappeared, so I cannot link to them here), he > said that Extensional Type Theory takes Intuitionistic Type Theory in a > different direction than HoTT does, formalizing the idea that types are > sets. Why does the HoTT book not mention this possibility? Why does ETT > not seem to get as much press as HoTT? > 2. When that same text introduces judgmental equality, it claims that > it is a decidable relation. It does not seem to prove this, and so I > suspected that perhaps the evidence was in Appendix A, where things are > done more formally (twice, even). The first of these two formalisms places > some restrictions on how one can introduce new judgmental equalities, which > seem sufficient to guarantee its decidability, but at no point is an > algorithm for deciding it given. Is the algorithm simply to apply the only > applicable rule over and over to reduce each side, and then compare for > exact syntactic equality? > 3. One of my favorite things about HoTT as a foundation for > mathematics actually comes just from DTT: Once you've formalized pi types, > you can define all of logic and (lots of) mathematics. But then the > hierarchy of type universes seem to require that we understand the natural > numbers, which is way more complicated than just pi types, and thus highly > disappointing to have to bring in at a foundational level. Am I right to > be disappointed about that or am I missing something? > > Thanks in advance for any help you have time and interest to provide! > > Nathan Carter > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com?utm_medium=email&utm_source=footer> > . > For more options, visit https://groups.google.com/d/optout. > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DjRvovt%2BA7RWi2y5ocgV6H%2BKY5YX6bULWyrTQ0fuEYSxg%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 8273 bytes --] <div dir="ltr"><div>1. There are at least two ways in which types are not sets. Firstly, when reasoning classically, we have a membership relation whereby we can postulate the membership of elements in a given set. It may seem similar to a : A but in this case writing a : B would make no sense, whereas in set theory membership can be disproven. This is quite a subtle notion and is closely related to the difference between structural and material set theories which Mike Shulman wrote a nice paper on <a href="https://arxiv.org/pdf/1808.05204.pdf">https://arxiv.org/pdf/1808.05204.pdf</a>. But I am sure someone else here will do a better job at explain that.</div><div><br></div><div>The second difference is what I think Harper was referring to, which is that sets are types which satisfy what is called Uniqueness of identity proofs (UIP). This means that given a : A and b : A, we can form the identity type Id(a, b). If we wish to show there is an equality between a and b we construct a term p : Id(a, b). But what if we can construct another equality q : Id(a, b)? UIP (a.k.a axiom K) ensures that there is always a term r : Id(p, q). Which in English means: Any two proofs of equality between elements of a set are themselves equal.</div><div><br></div><div>Why does this matter? Well because in Martin-Lof type theory (with univalent universes) (the type theory that HoTT is based on), you can construct seperate proofs of the same thing. Take for example the type 2. It has two terms 1_2 : 2 and 2_2 : 2. If we consider the ways in which 2 can be equal to itself, i.e. terms of Id(2, 2), we see that (with univalence) there are two possible ways. The first is just reflexivity and the second is "an equality" which swaps 1_2 with 2_2. These are both proofs of Id(2, 2) but they are definitely not the same. And in fact can't be shown to be the same without assuming UIP. </div><div> </div>2. One heuristic way to see that judgemental equality can be decided is by "completely computing" a given term, i.e. beta reduce it all the way down. Theorems such as Church-Rosser guarantee that the order of reductions does not matter. There are more properties such as "canonicity" which roughly state that fully reduced terms are identical. I am not an expert on these properties however but there are many experts on this list.<div><br></div><div>Checking whether two terms are judgementally equal is a commonly studied problem in type theory. There are ways to test equality without fully reducing down such as the one detailed here:</div><div><a href="https://link.springer.com/chapter/10.1007/978-3-540-70594-9_4">https://link.springer.com/chapter/10.1007/978-3-540-70594-9_4</a><br></div><div><br></div><div>3. Simply typed lambda calculus has "natural numbers" via the Church-encoding. The key difference between this and regular arithmetic is that you can't really define a function out of the type of such things. Or in other words, there is no recursion principle for the natural numbers. Adding such a rule would give you something like Godels system T. Universes only need a sucessor structure, and not really the full arithmetic capabilities of the natural numbers themselves.</div><div><br></div><div>These are just some of my thoughts on your questions, hopefully it will help.</div><div><br></div><div>Ali Caglayan</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jun 20, 2019 at 5:16 PM Nathan Carter <<a href="mailto:nathancarter5@gmail.com">nathancarter5@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div><br></div><div>Hello, HoTT community.</div><div><br></div><div>I've learned a bit about HoTT in bits of spare time over the past few years, and have come up with some questions I can't answer on my own. It was suggested that I ask them on this list. I will start with a few small questions, and if anyone in the community here has time to answer them, then I'll continue with others as needed. Thank you in advance for any help you can give.</div><div><br></div><div>(Where I'm coming from: I'm a mathematician; my dissertation was on intermediate logics, but I haven't focused on logic much for the past 15 years, instead doing mathematical software and some applied mathematics. I have a passion for clear exposition, so as I learn about HoTT, I process it by writing detailed notes to myself, explaining it as clearly as I can. When I can't explain something clearly, I flag it as a question. I'm bringing those questions here.)</div><div><br></div><div>Here are three to start.</div><div><ol><li>Very early in the HoTT book, it talks about the difference between types and sets, and says that HoTT encourages us to see sets as spaces. Yet in a set of lecture videos Robert Harper did that I watched on YouTube (which also seem to have disappeared, so I cannot link to them here), he said that Extensional Type Theory takes Intuitionistic Type Theory in a different direction than HoTT does, formalizing the idea that types are sets. Why does the HoTT book not mention this possibility? Why does ETT not seem to get as much press as HoTT?</li><li>When that same text introduces judgmental equality, it claims that it is a decidable relation. It does not seem to prove this, and so I suspected that perhaps the evidence was in Appendix A, where things are done more formally (twice, even). The first of these two formalisms places some restrictions on how one can introduce new judgmental equalities, which seem sufficient to guarantee its decidability, but at no point is an algorithm for deciding it given. Is the algorithm simply to apply the only applicable rule over and over to reduce each side, and then compare for exact syntactic equality?</li><li>One of my favorite things about HoTT as a foundation for mathematics actually comes just from DTT: Once you've formalized pi types, you can define all of logic and (lots of) mathematics. But then the hierarchy of type universes seem to require that we understand the natural numbers, which is way more complicated than just pi types, and thus highly disappointing to have to bring in at a foundational level. Am I right to be disappointed about that or am I missing something?</li></ol></div><div>Thanks in advance for any help you have time and interest to provide!</div><div><br></div><div>Nathan Carter</div><div><br></div></div> <p></p> -- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com" target="_blank">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com?utm_medium=email&utm_source=footer" target="_blank">https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com</a>.<br> For more options, visit <a href="https://groups.google.com/d/optout" target="_blank">https://groups.google.com/d/optout</a>.<br> </blockquote></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DjRvovt%2BA7RWi2y5ocgV6H%2BKY5YX6bULWyrTQ0fuEYSxg%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DjRvovt%2BA7RWi2y5ocgV6H%2BKY5YX6bULWyrTQ0fuEYSxg%40mail.gmail.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

On Thu, Jun 20, 2019 at 9:39 AM Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk> wrote: >> Very early in the HoTT book, it talks about the difference between types and sets, and says that HoTT encourages us to see sets as spaces. Yet in a set of lecture videos Robert Harper did that I watched on YouTube (which also seem to have disappeared, so I cannot link to them here), he said that Extensional Type Theory takes Intuitionistic Type Theory in a different direction than HoTT does, formalizing the idea that types are sets. Why does the HoTT book not mention this possibility? Why does ETT not seem to get as much press as HoTT? > > ETT or computational type theory relies on some notion of untyped computation which is then sorted by defining some semantic criteria for types. I don't know what Harper was talking about in those lectures, but although he does often talk about computational type theory that assigns types to untyped computations, usually "Extensional Type Theory" refers not to that, but to an intrinsically typed theory like HoTT that contains a "reflection rule" saying that any two typally (nee "propositionally") equal terms are in fact judgmentally equal. In particular, this forces all types to be sets (i.e. 0-truncated). The HoTT book doesn't talk about this possibility because, well, it's a book about HoTT, not about ETT. ETT (with reflection rule) has an important disadvantage that its typechecking is no longer decidable. There have been some serious attempts to work with such type theories (e.g. http://www.andromeda-prover.org/), but there are also several other often-preferred approach if you want all types to be sets, such as assuming Uniqueness of Identity Proofs as an axiom (or an equivalent axiom such as Streicher's K), allowing unrestricted pattern-matching as in vanilla Agda, or fancier things like Observational Type Theory or the recent XTT (https://arxiv.org/abs/1904.08562). There's nothing wrong with these theories; they just serve a different purpose than HoTT. Indeed, such theories are sometimes combined with HoTT in a "two-level" type theory (e.g. https://arxiv.org/abs/1705.03307). > There is the remaining issue that it is not known whether the cubical theory coincides with the simplicial interpretation which is the standard one in homotopy theory. I would express the issue by saying that it's not yet known whether cubical type theory has all of (or even any of) the intended higher-categorical models. The simplicial interpretation is only one of these models. >> One of my favorite things about HoTT as a foundation for mathematics actually comes just from DTT: Once you've formalized pi types, you can define all of logic and (lots of) mathematics. But then the hierarchy of type universes seem to require that we understand the natural numbers, which is way more complicated than just pi types, and thus highly disappointing to have to bring in at a foundational level. Am I right to be disappointed about that or am I missing something? As Thorsten said, you won't get much of anywhere in mathematics without the natural numbers in your foundation. However, I suspect your disappointment has to do with the occurrence of natural numbers at "meta-level" to index the universe levels, rather than the natural numbers type that appears inside the theory. For comparison, note that ZFC has in fact countably infinitely many axioms, so it also involves some natural numbers at meta-level. However, it is nearly always possible to eliminate such meta-infinities by incorporating them into the object theory; for instance, ZFC can be replaced by the finitely axiomatizable NBG, and one can formulate type theories that "internalize" the universe levels. For instance, in Agda there is a *type* of "universe levels" over which the universes are parametrized. Our semantic understanding of such universe structures is currently fairly primitive, but I expect it will improve. -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQzgvD8sqxbxn_2xOXQZ1XoSG4vnEe8LhcaQt_G2H8C6SQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1: Type: text/plain, Size: 3015 bytes --] Thank you all (Thorsten, Ali, Michael, and some folks off-list, too) for the helpful responses. I'll try to summarize here to be sure I've understood. Please feel free to correct anything I say incorrectly. 1. Regarding ETT People mentioned the loss of important computational properties if one adopts ETT, and I can certainly see why that would be a big deal. While the subtleties relating 0-truncation, UIP, K, and reflection rules are not 100% clear to me, I at least have a high-level intuition, which is what I want at this point. 2. Decidability of judgmental equality I got seemingly (to me?) conflicting answers. One person off-list and one on-list said (I think) that applying all possible beta reductions and symbol definitions would be sufficient to decide judgmental equality; another said that this is not the case (again, I think). But I was given a reference to a paper <https://link.springer.com/chapter/10.1007/978-3-540-70594-9_4>, so I can find out more on my own. 3. Numbers as universe indices The responses showed that my question wasn't clear. Saying something like "from pi types you can do all the things" was sloppy. I was trying to express that, once you've defined pi types, you've (a) learned the rules about substitution, capture, etc., plus (b) encountered the principles by which types are defined in general (which I have other questions about...but later). And from those two things, you can do lots of stuff. Several folks said that "the natural numbers" is an overstatement, since successor and maximum are enough; responses suggested various things simpler than N that have these. But Michael helped express my unease more precisely: I'm not trying to do mathematics without the natural numbers; that would be silly and was part of my question's sloppiness. Rather, I'm appreciating that DTT lets us build a foundation with fewer pieces than usual (cleaner than a dozen-or-so rules of ND with guards on variables appearing free in undischarged assumptions and so on, plus mathematical axioms). To need a number system very early on seemed to lose some of this purity, especially since it seemed to be in the metatheory. I do not (yet) fully understand Michael's answer about Agda's type of universe levels, but I guess that it avoids paradoxes by being one step removed from a type of all universes, which sounds clever. These replies will help me make progress on my notes, so thank you very much again. Once I've gotten to a good point for asking more questions, I will do so. Nathan -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/6682FD3B-6A4C-49B4-B54D-E78FB4E71046%40gmail.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 4439 bytes --] <html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div class=""><div class="">Thank you all (Thorsten, Ali, Michael, and some folks off-list, too) for the helpful responses. I'll try to summarize here to be sure I've understood. Please feel free to correct anything I say incorrectly.</div><div class=""><br class=""></div><div class="">1. Regarding ETT</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>People mentioned the loss of important computational properties if one adopts ETT, and I can certainly see why that would be a big deal. While the subtleties relating 0-truncation, UIP, K, and reflection rules are not 100% clear to me, I at least have a high-level intuition, which is what I want at this point.</div><div class=""><br class=""></div><div class="">2. Decidability of judgmental equality</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>I got seemingly (to me?) conflicting answers. One person off-list and one on-list said (I think) that applying all possible beta reductions and symbol definitions would be sufficient to decide judgmental equality; another said that this is not the case (again, I think). But I was given a reference to <a href="https://link.springer.com/chapter/10.1007/978-3-540-70594-9_4" class="">a paper</a>, so I can find out more on my own.</div><div class=""><br class=""></div><div class="">3. Numbers as universe indices</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>The responses showed that my question wasn't clear. Saying something like "from pi types you can do <i class="">all the things"</i> was sloppy. I was trying to express that, once you've defined pi types, you've (a) learned the rules about substitution, capture, etc., plus (b) encountered the principles by which types are defined in general (which I have other questions about...but later). And from those <i class="">two </i>things, you can do lots of stuff.</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>Several folks said that "the natural numbers" is an overstatement, since successor and maximum are enough; responses suggested various things simpler than N that have these.</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>But Michael helped express my unease more precisely: I'm not trying to do mathematics without the natural numbers; that would be silly and was part of my question's sloppiness. Rather, I'm appreciating that DTT lets us build a foundation with fewer pieces than usual (cleaner than a dozen-or-so rules of ND with guards on variables appearing free in undischarged assumptions and so on, plus mathematical axioms). To need a number system very early on seemed to lose some of this purity, <i class="">especially </i>since it seemed to be in the metatheory. I do not (yet) fully understand Michael's answer about Agda's type of universe levels, but I guess that it avoids paradoxes by being one step removed from a type of all universes, which sounds clever.</div><div class=""><br class=""></div><div class="">These replies will help me make progress on my notes, so thank you very much again. Once I've gotten to a good point for asking more questions, I will do so.</div><div class=""><br class=""></div><div class="">Nathan</div></div><div class=""><br class=""></div></body></html> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/6682FD3B-6A4C-49B4-B54D-E78FB4E71046%40gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/6682FD3B-6A4C-49B4-B54D-E78FB4E71046%40gmail.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

I think the reason for the mixed messages re: #2 is that different type theories have different rules for judgmental equality. If the only rules for judgmental equality are "directed" ones like beta-reduction, then (assuming a normalization result) to check equality it generally suffices to reduce two terms to normal form and compare the normal forms. But if there are also other rules for judgmental equality, like eta-conversion, that are difficult to formulate in a "directed" way, then you generally need a fancier equality-checking algorithm. And some rules for judgmental equality, like equality reflection in ETT, prevent there from being any algorithm at all. The HoTT Book assumes eta-conversion, so simple reduction to normal forms is probably not sufficient. There are well-understood algorithms for equality-checking in MLTT with eta (generally built on ideas like https://ncatlab.org/nlab/show/bidirectional+typechecking); but Book HoTT also adds judgmental computation rules for point-constructors of HITs, and while it seems intuitive that those should be regarded as beta-reduction-like, I'm not aware that anyone has precisely formulated an equality-checking algorithm for Book HoTT. On Thu, Jun 20, 2019 at 4:11 PM Nathan Carter <nathancarter5@gmail.com> wrote: > > > Thank you all (Thorsten, Ali, Michael, and some folks off-list, too) for the helpful responses. I'll try to summarize here to be sure I've understood. Please feel free to correct anything I say incorrectly. > > 1. Regarding ETT > People mentioned the loss of important computational properties if one adopts ETT, and I can certainly see why that would be a big deal. While the subtleties relating 0-truncation, UIP, K, and reflection rules are not 100% clear to me, I at least have a high-level intuition, which is what I want at this point. > > 2. Decidability of judgmental equality > I got seemingly (to me?) conflicting answers. One person off-list and one on-list said (I think) that applying all possible beta reductions and symbol definitions would be sufficient to decide judgmental equality; another said that this is not the case (again, I think). But I was given a reference to a paper, so I can find out more on my own. > > 3. Numbers as universe indices > The responses showed that my question wasn't clear. Saying something like "from pi types you can do all the things" was sloppy. I was trying to express that, once you've defined pi types, you've (a) learned the rules about substitution, capture, etc., plus (b) encountered the principles by which types are defined in general (which I have other questions about...but later). And from those two things, you can do lots of stuff. > Several folks said that "the natural numbers" is an overstatement, since successor and maximum are enough; responses suggested various things simpler than N that have these. > But Michael helped express my unease more precisely: I'm not trying to do mathematics without the natural numbers; that would be silly and was part of my question's sloppiness. Rather, I'm appreciating that DTT lets us build a foundation with fewer pieces than usual (cleaner than a dozen-or-so rules of ND with guards on variables appearing free in undischarged assumptions and so on, plus mathematical axioms). To need a number system very early on seemed to lose some of this purity, especially since it seemed to be in the metatheory. I do not (yet) fully understand Michael's answer about Agda's type of universe levels, but I guess that it avoids paradoxes by being one step removed from a type of all universes, which sounds clever. > > These replies will help me make progress on my notes, so thank you very much again. Once I've gotten to a good point for asking more questions, I will do so. > > Nathan > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/6682FD3B-6A4C-49B4-B54D-E78FB4E71046%40gmail.com. > For more options, visit https://groups.google.com/d/optout. -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQzbSbOCFrBK_X2-45eBovJ5e799wXrQPec9h1-sZUGH5Q%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.