In "Naturals", the first chapter of Part I, two inference rules are offered as a definition of the natural numbers, for which the following Agda code is provided as an equivalent.
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
Something seems to be missing.
On its face, the Agda code says that zero is a natural, and that for any natural n, suc n is a natural. That is also what the inference rules seem to say, and what the prose says they say. But those two rules don't by themselves provide the natural numbers: a data type with a single instance, for which suc is defined as the identity function, would satisfy those rules, as would many other collections of values and definitions of suc. (Boolean, for example, taking true, false, and not as alternate spellings of zero, suc zero, and suc.) To make a formal definition of the natural numbers that matches the good informal understanding we all are said to possess, I think some things are missing:
A statement that nothing else is a natural number. (On re-reading the chapter, I find that the prose does say this, even if it's left implicit in the Agda code. So that's OK. Maybe I just missed the others, too.)
A statement that there is no natural n whose successor is zero.
A statement that if suc n = suc m, then n = m.
(Cf. Peano's arithmetic axioms 9, 8, and 7. The Agda code seems to handle 1 and 6.)
There seem to be two possibilities: (1) this is a partial specification of the natural numbers, and for pedagogical reasons it is thought better not to go into the details of the missing bits. In this case, I think it would be helpful to readers like this one to say explicitly something like "There are some other things that have to be said, in order to make ℕ match our intuitions about the naturals, but they would take us too far afield, so we won't go into those details at this point."
Or (2) there is some magic going on, such that Agda knows a priori that zero can never be the successor of any natural and that the constructor function suc is an injection. Neither of those seems at all plausible to me, but then again I know nothing about Agda but what I have read in this book and a few other beginner tutorials. I have no idea what kinds of framing assumptions are present in Agda without ever being written out in Agda code. So I'll settle for claiming that that kind of magic doesn't really go without saying, since it would go well beyond what is in the inference rules cited or what can be seen with an untrained eye in the Agda code shown. If this kind of magic is happening, then the Agda code does not mean the same thing as the inference rules, but something more. That difference needs at least to be mentioned, in the same way that the prose now mentions that "Further, these two rules give the only ways of creating natural numbers". In this case, I cannot suggest wording, since I don't know what needs saying, only that something needs saying.
In "Naturals", the first chapter of Part I, two inference rules are offered as a definition of the natural numbers, for which the following Agda code is provided as an equivalent.
Something seems to be missing.
On its face, the Agda code says that
zerois a natural, and that for any naturaln,suc nis a natural. That is also what the inference rules seem to say, and what the prose says they say. But those two rules don't by themselves provide the natural numbers: a data type with a single instance, for which suc is defined as the identity function, would satisfy those rules, as would many other collections of values and definitions of suc. (Boolean, for example, takingtrue,false, andnotas alternate spellings ofzero,suc zero, andsuc.) To make a formal definition of the natural numbers that matches the good informal understanding we all are said to possess, I think some things are missing:nwhose successor iszero.suc n = suc m, thenn = m.(Cf. Peano's arithmetic axioms 9, 8, and 7. The Agda code seems to handle 1 and 6.)
There seem to be two possibilities: (1) this is a partial specification of the natural numbers, and for pedagogical reasons it is thought better not to go into the details of the missing bits. In this case, I think it would be helpful to readers like this one to say explicitly something like "There are some other things that have to be said, in order to make ℕ match our intuitions about the naturals, but they would take us too far afield, so we won't go into those details at this point."
Or (2) there is some magic going on, such that Agda knows a priori that zero can never be the successor of any natural and that the constructor function suc is an injection. Neither of those seems at all plausible to me, but then again I know nothing about Agda but what I have read in this book and a few other beginner tutorials. I have no idea what kinds of framing assumptions are present in Agda without ever being written out in Agda code. So I'll settle for claiming that that kind of magic doesn't really go without saying, since it would go well beyond what is in the inference rules cited or what can be seen with an untrained eye in the Agda code shown. If this kind of magic is happening, then the Agda code does not mean the same thing as the inference rules, but something more. That difference needs at least to be mentioned, in the same way that the prose now mentions that "Further, these two rules give the only ways of creating natural numbers". In this case, I cannot suggest wording, since I don't know what needs saying, only that something needs saying.