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)
added earlier reference for the introduction of the notion of W-types:
following a hint in another thread (here)
Hubert Wasilewski
In reality “Hubert Wasilewski” in #27 made no discernible edit.
By why does the text of #27 copy your text from #26?
It keeps happening (I have been flagging it previously): Newbie users appear who announce an otherwise empty edit by copying my latest edit log.
It is either a strange bug or a strange prank.
I had meant to bring it to the attention of the the technical team, but didn’t get around to yet.
If you try to edit without entering a name in the “Submit as ….” text field, the following things happen:
A yellow box appears at the top of the page with the text “Please enter your name. (Due to a flood of low quality edits, we restrict anonymous edits.)”
The comment of the last edit made on that page is copied into the comment box at the bottom of the page above the “Submit as ….” text field. Sometimes this is still empty because the last editor did not make a comment.
Thanks, that’s useful to know! I have brought this to the attention of the technical team.
The comment of the last edit made on that page is copied into the comment box at the bottom of the page above the “Submit as ….” text field. Sometimes this is still empty because the last editor did not make a comment.
Apparently, that was how the announcement box was designed. It worked as intended when the failed edit itself contained an announcement message (then that one would be displayed). I think this bug just showed more now because there are more ways for an edit to fail (e.g., empty username).
I made a change that should fix this. Thanks for letting us now.
Now, when you try to edit without entering a name in the “Submit as ….” text field and encounter the yellow text box at the top, the previous editor’s comments no longer appear in the comments box. However, the contents of the article disappear from the article text’s box as well.
1 to 34 of 34