Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 8 of 8
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?
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$.
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”?
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.
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.
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.
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!
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!
1 to 8 of 8