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.
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).
Thanks. Maybe we should remove some of that detail from inductive type, then, and say “see natural numbers type”.
Yes. I can do it later when I have time. But I won’t mind if somebody else does it…
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.
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.
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
added pointer to:
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
Re #6, yes, Happy New Year everyone!
1 to 10 of 10