Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorTim Johns
   • CommentTimeOct 2nd 2023
   • PermaLink
   Author: Tim Johns
   Format: MarkdownItexI've been using the book "Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy" by David Corfield as one of my primary resources and motivations for studying HoTT and I think I have found a fundamental mistake in some of the explanations for dependent pairs. On page 45, the author discusses a type of dates, where the dependent pair is defined as $\sum_{m : Month} d : Day(m)$ . Sample elements of the type are given: $(February, 24)$ and $(August, 5)$. It is my understanding that in type theory, every element belongs to exactly one type. This presents a problem in this treatment of dates. If we consider the element $(August, 24)$, we now have the problem that $24$ seems to belong to both types $Day(February)$ and $Day(August)$. In other words, we have $24 : Day(February)$ and $24 : Day(August)$ in the same context. To remedy this, we could split up the $Day$ elements into their respective months, as in: $(February, 24_feb)$ and $(August, 24_aug)$, where $24_feb : Day(February)$ and $24_aug : Day(August)$. But now, we have no use for the first part of each pair as the second part carries all the information. It seems to me that the type of dates can't be treated in an elegant way as the author intended (I can think of other practical ways, but they involve $Fin$ or nested dependent pairs). I believe the same problem occurs on page 46, in the treatment of "day and hour". The type is written in a dependent way, as $\sum_{d : Day} d : Hour(d)$ . The given sample elements are: $(Monday, 15:00)$ and $(Saturday, 09:00)$. Again, if we consider an element such as $(Tuesday, 15:00)$, we have the problem that $15:00$ belongs to $Hour(Monday)$ _and_ $Hour(Tuesday)$. The author does explain that this is a special case where the types have no genuine dependence, but it is my understanding that the type should be properly defined as $\sum_{d : Day} d : Hour$ (or the equivalent, $Day \times Hour$). This way, $15:00$ simply belongs to the type $Hour$ in both elements. Is my thinking in all this correct?

   I’ve been using the book “Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy” by David Corfield as one of my primary resources and motivations for studying HoTT and I think I have found a fundamental mistake in some of the explanations for dependent pairs.

   On page 45, the author discusses a type of dates, where the dependent pair is defined as $\sum_{m : Month} d : Day(m)$ . Sample elements of the type are given: $(February, 24)$ and $(August, 5)$. It is my understanding that in type theory, every element belongs to exactly one type. This presents a problem in this treatment of dates. If we consider the element $(August, 24)$, we now have the problem that $24$ seems to belong to both types $Day(February)$ and $Day(August)$. In other words, we have $24 : Day(February)$ and $24 : Day(August)$ in the same context. To remedy this, we could split up the $Day$ elements into their respective months, as in: $(February, 24_feb)$ and $(August, 24_aug)$, where $24_feb : Day(February)$ and $24_aug : Day(August)$. But now, we have no use for the first part of each pair as the second part carries all the information. It seems to me that the type of dates can’t be treated in an elegant way as the author intended (I can think of other practical ways, but they involve $Fin$ or nested dependent pairs).

   I believe the same problem occurs on page 46, in the treatment of “day and hour”. The type is written in a dependent way, as $\sum_{d : Day} d : Hour(d)$ . The given sample elements are: $(Monday, 15:00)$ and $(Saturday, 09:00)$. Again, if we consider an element such as $(Tuesday, 15:00)$, we have the problem that $15:00$ belongs to $Hour(Monday)$ and $Hour(Tuesday)$. The author does explain that this is a special case where the types have no genuine dependence, but it is my understanding that the type should be properly defined as $\sum_{d : Day} d : Hour$ (or the equivalent, $Day \times Hour$). This way, $15:00$ simply belongs to the type $Hour$ in both elements.

   Is my thinking in all this correct?

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeOct 2nd 2023
   • PermaLink
   Author: Urs
   Format: MarkdownItexWhile I don't have the book in front of me right now, this does not seem to be a mistake in the book but a misunderstanding on your part. Take a step back from those picturesque examples and just rethink what it means to have a term of dependent pair type $\sum_n T(n)$. Then observe that nothing in this definition changes when the $N$-dependent type $T$ happens to take the same value at all $n$.

   While I don’t have the book in front of me right now, this does not seem to be a mistake in the book but a misunderstanding on your part.

   Take a step back from those picturesque examples and just rethink what it means to have a term of dependent pair type $\sum_n T(n)$. Then observe that nothing in this definition changes when the $N$-dependent type $T$ happens to take the same value at all $n$.

3. • CommentRowNumber3.
   • CommentAuthorTim Johns
   • CommentTimeOct 2nd 2023
   • PermaLink
   Author: Tim Johns
   Format: MarkdownItexI think that only addresses the second part of what I wrote (the "day and hour"), where the two types are not genuinely dependent. And I think you're completely right. My understanding of that is still shaky, but I can see your point. However, the case of the dates is not the same because it is a genuine dependent type. To make this more clear, I have used Agda to verify my thinking. This forum doesn't seem to favour code posts so here's a link to a gist with the Agda code: [https://gist.github.com/SlimTim10/bc3c587af76afc6d0ef63531128f41c5](https://gist.github.com/SlimTim10/bc3c587af76afc6d0ef63531128f41c5) I guess the big question is whether constructor overloading is to be understood as a feature of Agda or inherent in type theory itself? In other words, in the same context, could I define $24\colon\mathbb{N}$ and $24\colon\FebDay$ and $24\colon\AugDay$ ? Or would I need 3 different constructors for each "24"?

   I think that only addresses the second part of what I wrote (the “day and hour”), where the two types are not genuinely dependent. And I think you’re completely right. My understanding of that is still shaky, but I can see your point.

   However, the case of the dates is not the same because it is a genuine dependent type. To make this more clear, I have used Agda to verify my thinking. This forum doesn’t seem to favour code posts so here’s a link to a gist with the Agda code:

   https://gist.github.com/SlimTim10/bc3c587af76afc6d0ef63531128f41c5

   I guess the big question is whether constructor overloading is to be understood as a feature of Agda or inherent in type theory itself? In other words, in the same context, could I define $24\colon\mathbb{N}$ and $24\colon\FebDay$ and $24\colon\AugDay$ ? Or would I need 3 different constructors for each “24”?

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeOct 2nd 2023
   • PermaLink
   Author: Urs
   Format: MarkdownItexI still don't think there is something wrong with the book on this point. Still not having the book in front of me I am guessing that these types are *defined* as $$ \begin{array}{l} FebDay \,\equiv\, (n \colon \mathbb{N}) \times ( n \leq 28) \\ AugDay \,\equiv\, (n \colon \mathbb{N}) \times ( n \leq 31) \end{array} $$ or similar, in which case the same term $24 \colon \mathbb{N}$ does inhabit all these types, once paired with a certificate that it is in the admissible range.

   I still don’t think there is something wrong with the book on this point.

   Still not having the book in front of me I am guessing that these types are defined as

   $$\begin{array}{l} FebDay \,\equiv\, (n \colon \mathbb{N}) \times ( n \leq 28) \\ AugDay \,\equiv\, (n \colon \mathbb{N}) \times ( n \leq 31) \end{array}$$

   or similar, in which case the same term $24 \colon \mathbb{N}$ does inhabit all these types, once paired with a certificate that it is in the admissible range.

5. • CommentRowNumber5.
   • CommentAuthorTim Johns
   • CommentTimeOct 2nd 2023
   • (edited Oct 3rd 2023)
   • PermaLink
   Author: Tim Johns
   Format: MarkdownItexThat's actually part of the problem: the type for days is not defined in the book. I'd love to know what definition David had in mind when writing it. The practical type for MonthAndDay I had in mind is along your idea: $$ \begin{array}{l} Day \colon Month \to Type \\ Day(feb) \equiv \sum_{d \colon \mathbb{N}} d \geq 1 \times d \leq 28 \\ Day(aug) \equiv \sum_{d \colon \mathbb{N}} d \geq 1 \times d \leq 31 \\ \\ \\ MonthAndDay \colon Type \\ MonthAndDay \equiv \sum_{m \colon Month} Day(m) \end{array} $$ Where elements of $MonthAndDay$ look like: $$ \begin{array}{l} feb24 \colon MonthAndDay \\ feb24 \equiv feb , (24 , (\star , \star)) \\ \\ \\ aug24 \colon MonthAndDay \\ aug24 \equiv aug , (24 , (\star , \star)) \\ \end{array} $$ So, yes, that looks close to what David had in mind, but there's clearly more information in these types and elements than he wrote in his book, isn't there? Is this perhaps a case of simplified high-level definitions that I'm not used to reading as I'm not an academic mathematician? I would have to say, as an introduction to dependent pairs, leaving out such information can be very misleading.

   That’s actually part of the problem: the type for days is not defined in the book. I’d love to know what definition David had in mind when writing it.

   The practical type for MonthAndDay I had in mind is along your idea:

   $$\begin{array}{l} Day \colon Month \to Type \\ Day(feb) \equiv \sum_{d \colon \mathbb{N}} d \geq 1 \times d \leq 28 \\ Day(aug) \equiv \sum_{d \colon \mathbb{N}} d \geq 1 \times d \leq 31 \\ \\ \\ MonthAndDay \colon Type \\ MonthAndDay \equiv \sum_{m \colon Month} Day(m) \end{array}$$

   Where elements of $MonthAndDay$ look like:

   $$\begin{array}{l} feb24 \colon MonthAndDay \\ feb24 \equiv feb , (24 , (\star , \star)) \\ \\ \\ aug24 \colon MonthAndDay \\ aug24 \equiv aug , (24 , (\star , \star)) \\ \end{array}$$

   So, yes, that looks close to what David had in mind, but there’s clearly more information in these types and elements than he wrote in his book, isn’t there? Is this perhaps a case of simplified high-level definitions that I’m not used to reading as I’m not an academic mathematician? I would have to say, as an introduction to dependent pairs, leaving out such information can be very misleading.

6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeOct 2nd 2023
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexApologies if you found it misleading. You seem to have worked out one presentation. Let me pre-empt another potential confusion in what isn't just a lack of detail, but a mistake in the elimination rule for dependent product on p. 55.

   Apologies if you found it misleading. You seem to have worked out one presentation.

   Let me pre-empt another potential confusion in what isn’t just a lack of detail, but a mistake in the elimination rule for dependent product on p. 55.

7. • CommentRowNumber7.
   • CommentAuthorTim Johns
   • CommentTimeOct 2nd 2023
   • (edited Oct 3rd 2023)
   • PermaLink
   Author: Tim Johns
   Format: MarkdownItexNo worries, David! Your text has been one of my favourite books of the past two years. It is truly a gem. This particular concern was just a matter of me questioning whether I have something fundamentally wrong in my understanding or if it is the way it's explained in the book. Thanks. > Let me pre-empt another potential confusion in what isn’t just a lack of detail, but a mistake in the elimination rule for dependent product on p. 55. Thanks for that, too!

   No worries, David! Your text has been one of my favourite books of the past two years. It is truly a gem. This particular concern was just a matter of me questioning whether I have something fundamentally wrong in my understanding or if it is the way it’s explained in the book. Thanks.

   Let me pre-empt another potential confusion in what isn’t just a lack of detail, but a mistake in the elimination rule for dependent product on p. 55.

   Thanks for that, too!

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeOct 4th 2023
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexThat's very kind of you to say. I'm sure there's plenty to improve for a second edition, perhaps one with a new chapter on [linear HoTT](https://ncatlab.org/schreiber/show/Quantum+Certification+via+Linear+Homotopy+Types)!

   That’s very kind of you to say.

   I’m sure there’s plenty to improve for a second edition, perhaps one with a new chapter on linear HoTT!