adding section about the extensionality principle of the natural numbers
]]>Re #6, yes, Happy New Year everyone!
]]>added pointer to page and verse in the the original articles by Coquand & Paulin and by Dybjer where the natural numbers type is considered
the article
is the only one which I have seen, so far, which pauses to explain why the naive non-dependent recursion scheme is not sufficient (which is maybe the most important point of the whole business, but traditionally goes without any comment). I have added a brief Remark on this point here
]]>added pointer to:
Best wishes for the New Year to everyone!
$\,$
I have re-typeset the inference rules for the natural numbers type:
more whitespace
hierarchized parenthesis
more suggestive term names
in order to guide the eye about how the syntax tree is meant to be branching and to make it more readily graspable what all the symbols want to mean
Currently it looks as follows:
and
$\frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(x) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) \;\vdash\; succ_P(x,p) \,\colon\, P(s x) \;; \;\;\;\; \vdash\; n \,\colon\, \mathbb{N} \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} ind_{(P, 0_P, succ_P)}\big(succ(n)\big) \,=\, succ_P\big(n,\, rec^n_P(0_P,\, succ_P)\big) }$will be adjusting the rest of the entry accordingly
]]>previously the discussion (here) of the categorical semantics of recursion was too restrictive, as it didn’t take the possible $\mathbb{N}$-dependency of the $F$-algebra’s successor function into account, i.e. it didn’t consider passing to the slice.
I have now expanded this out by adding discussion of the categorical semantics of the full recursion principle (now starting here).
In the course of this I made various slight adjustments and rearrangements throughout the entry, in an attempt to polish it up a little.
]]>I fixed the suspected syntax errors in the elimination rule, added the requested computation rules, threw in the type formation rule for good measure, and added some formatting features (line breaks and semicolons) for increased readability.
]]>Yes. I can do it later when I have time. But I won’t mind if somebody else does it…
]]>Thanks. Maybe we should remove some of that detail from inductive type, then, and say “see natural numbers type”.
]]>created natural numbers type (we had had type of natural numbers, but only as a redirect to natural numbers object).
I filled the entry (only) with material copied over from inductive type (for the moment).
]]>