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 $C$ to $\mathcal{C}$ as it seemed rather bad style to have a category named $C$ with objects named $A$, $B$ and $D$.
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 “$\mathcal{W}$-type”, throughout
switched the ordering of the subsections “In category theory”, “In type theory”.
The $\mathcal{W}$-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:
“$C$” for the type of constructors
“$A$” for the type of arities.
introduced formatting of $\mathcal{W}$-type denotation as “$\underset{c \colon C}{\mathcal{W}} \, A(c)$”
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, $W$-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:
$\frac { C \,\colon\, Type \;; \;\;\; c \,\colon\, C \;\;\vdash\;\; A(c) \,\colon\,Type \mathclap{\phantom{\vert_{\vert}}} } { \mathclap{\phantom{\vert^{\vert}}} \underset{c \colon C}{\mathcal{W}}\, A(c) \,\colon\, Type }$ $\frac{ \vdash\; root \,\colon\, C \;; \;\; subtr \,\colon\, A(c) \to \underset{c \colon C}{\mathcal{W}}\, A(c) }{ \mathclap{\phantom{\vert^{\vert}}} tree\big(root ,\, subtr\big) \,\colon\, \underset{c \colon C}{\mathcal{W}}\, A(c) }$ $\frac{ \begin{array}{l} t \,\colon\, \underset{c \colon C}{\mathcal{W}}\, A(c) \;\vdash\; D(t) \,\colon\, Type \;; \\ root \,\colon\, C \,, \; subt \,\colon\, A(c) \to \underset{c \colon C}{\mathcal{W}}\, A(c) \,, \; subt_D \,\colon\, \underset{a \colon A(root)}{\prod} D\big(subt(a)\big) \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \;\;\vdash\;\; tree_D\big(root,\,subt ,\, subt_D\big) \,\colon\, D\big(tree(c,\, subt)\big) \mathclap{\phantom{\vert_{\vert}}} \end{array} }{ \mathclap{\phantom{\vert^{\vert}}} t \,\colon\, \underset{c \colon C}{\mathcal{W}}\, A(c) \;\vdash\; wrec_{(D,tree_D)}(t) \,\colon\, D(t) }$(4) computation rule:
$\frac{ \begin{array}{l} t \,\colon\, \underset{c \colon C}{\mathcal{W}}\, A(c) \;\vdash\; D(t) \,\colon\, Type \;; \\ root \,\colon\, C \,,\; subt \,\colon\, A(c) \to \underset{c \colon C}{\mathcal{W}}\, A(c) \,, \; subt_D \,\colon\, \underset{a\colon A(c)}{\Pi} D\big(subt(a)\big) \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \;\;\vdash\;\; tree_D\big(root,\,subt,\,subt_D\big) \,\colon\, D\big(tree(root,\, subt)\big) \mathclap{\phantom{\vert_{\vert}}} \end{array} }{ \begin{array}{l} \mathclap{\phantom{\vert^{\vert}}} root \,\colon\, C \,, \;\; subtr \,\colon\, A(c) \to \underset{c \colon C}{\mathcal{W}}\, A(c) \\ \;\;\;\;\;\;\;\;\;\;\; \;\;\vdash\;\; wrec_{(D,tree_D)}\big( tree(root, \, subtr) \big) \;=\; tree_D \Big( root ,\, subt ,\, \lambda a . wrec_{(D,tree_D)}\big(subtr(a)\big) \Big) \end{array} }$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:
$F(Y) = A_n \times Y^{\times n} + \dots + A_1 \times Y + A_0$can be constructed as polynomial endofunctors in the above sense in any $\Pi$-pretopos.
I changed the $\Pi$-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 $\sigma$-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