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 W-type.
And a related query at pretopos.
Added to W-type a section Properties with a pointer to Danielsson’s recent post.
added to W-type pointers to
the article by Gambino-Hyland on dependent W-types
the article by van den Berg and Moerdijk on W-types in model categories (those given by fibrations)
Also made the following trivial edit: changed the name of the ambient category from to as it seemed rather bad style to have a category named with objects named , and .
I’ll have a question or comment on W-types in linear type theory, but I’ll put that in a separate thread…
Heh, you changed the name from a recognizable letter to a nondescript grey box, according to my Firefox for Android. But that’s OK, I don't think that we should actually cater to that.
Thanks for editing.
Allow me to mention some hints on formatting references:
leave a whitespace to any previous text, not to have the output clutter
a *
followed by a whitespace right at the beginning of the line makes a bullet item for the reference to fit into the rest of the list
enclosing author names in double square brackets hyperlinks them to their pages
explicit hyperlinks need the http://
-prefix to be parsed
I have slightly reformatted accordingly, now the source looks like so
* [[Michael Abbott]], [[Thorsten Altenkirch]], and [[Neil Ghani]],
_Representing Nested Inductive Types using W-types_
([pdf](http://www.cs.nott.ac.uk/~psztxa/publ/icalp04.pdf))
and renders like so:
Spencer Breiner pointed out on Zulip that this page claims that natural numbers (and lists) are W-types, when type-theoretically they are actually not. In type theory, a W-type has only one constructor, while nat and lists have two constructors. They can be encoded as W-types using a sum-type to wrap up the two constructors into one, but the result doesn’t have the same computation rules and requires function extensionality for its correctness. So I removed these examples from this page and put the corresponding text at inductive type.
A W-type is a set or type which is defined inductively in a well-founded way based on a type of “constructors” and a type of “arities”. It is thus a particular kind of inductive type, with one constructor having a certain canonical form.
How’s that “thus” working? Why “one constructor” in this concept.
Maybe we should just omit “thus”. Would it make sense that way?
Have written it as
A W-type is a set or type which is defined inductively in a well-founded way based on a type of “constructors” and a type of “arities”, with one constructor having a certain canonical form. As such it is a particular kind of inductive type.
The page still contains a query from you Mike:
Is the term “W-type” still used in this generality? Or are they just called “inductive types”?
Is this resolved yet?
Thanks for pointing that out, have now resolved it.
I have added publication data to:
I am guessing that this is the reference which was meant to be referred to at the end of this paragraph (where it had a broken anchor to [AAG](#AAG)
) and so I fixed the link accordingly
did a fair bit of rewording and adjustment in the Idea-section (here) for better (logical) flow
switched to calligraphic “-type”, throughout
switched the ordering of the subsections “In category theory”, “In type theory”.
The -type inference rules here had a query box comment:
Andreas Abel: A and B are used exactly the other way round in the introductory text to this page. (Before, A was the arity, now B is the arity.) Harmonize!?
Indeed. Am harmonizing this now by using, throughout:
“” for the type of constructors
“” for the type of arities.
introduced formatting of -type denotation as “”
fixed these bibitems:
Ieke Moerdijk, Erik Palmgren, Wellfounded trees in categories, Annals of Pure and Applied Logic 104 1-3 (2000) 189-218 [doi:10.1016/S0168-0072(00)00012-9]
Benno van den Berg, Ieke Moerdijk, -types in sheaves [arXiv:0810.2398]
adjusted the typesetting of the type inference rules, in particular:
added more widespace to make it easier on the eye to recognize the syntax tree branching
chose more suggestive term names
now it looks as follows:
(1) type formation rule:
(4) computation rule:
added pointer to:
Jasper Hugunin, Why Not W?, Leibniz International Proceedings in Informatics (LIPIcs) 188 (2021) [doi:10.4230/LIPIcs.TYPES.2020.8, pdf]
Peter Dybjer, Representing inductively defined sets by wellorderings in Martin-Löf’s type theory, Theoretical Computer Science 176 1–2 (1997) 329-335 [doi:10.1016/S0304-3975(96)00145-4]
In the sentence
More generally, endofunctors that look like polynomials in the traditional sense:
can be constructed as polynomial endofunctors in the above sense in any -pretopos.
I changed the -pretopos to just a pretopos, since that is all one needs for the finite products and coproducts.
I plan to add in the morphism that makes the endofunctor in the previous comment polynomial, having now double checked it really works for an arbitrary pretopos. For a -pretopos (ie countable coproducts and corresponding extensivity) one gets analytic endofunctors (those that are formal power series) being polynomial for free as well. Then I’ll check about existence of W-types for these based just on having a parameterised NNO.
added earlier reference for the introduction of the notion of W-types:
following a hint in another thread (here)
1 to 26 of 26