added earlier reference for the introduction of the notion of W-types:

- Per Martin-Löf, pp. 171 of:
*Constructive Mathematics and Computer Programming*, in:*Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science (1979)*, Studies in Logic and the Foundations of Mathematics**104**(1982) 153-175 $[$doi:10.1016/S0049-237X(09)70189-2, ISBN:978-0-444-85423-0$]$

following a hint in another thread (here)

]]>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.

]]>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.

]]>mentioned that the dependent product is not dependent in the plain case by factoring through the reader monad

]]>organized all references on semantics of W-types by initial endofunctor algebras: here

(cf. nForum announcement here)

]]>made explicit the example of the natural numbers W-type with a numbered environment (here)

]]>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]

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:**

]]>

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]

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

*c*onstructors“$A$” for the type of

*a*rities.

introduced formatting of $\mathcal{W}$-type denotation as “$\underset{c \colon C}{\mathcal{W}} \, A(c)$”

]]>I have added publication data to:

- Michael Abbott, Thorsten Altenkirch, Neil Ghani:
*Representing Nested Inductive Types using W-types*, in*Automata, Languages and Programming*, ICALP 2004, Lecture Notes in Computer Science**3142**, Springer (2004) [doi:10.1007/978-3-540-27836-8_8, pdf]

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

Thanks for pointing that out, have now resolved it.

]]>Clarified the situation with indices, parameters, and non-uniform parameters.

]]>Have written it as

A

W-typeis 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?

]]>Maybe we should just omit “thus”. Would it make sense that way?

]]>A

W-typeis 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.

]]>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.

]]>Added reference

- Jasper Hugunin,
*IWTypes*, https://github.com/jashug/IWTypes

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 listenclosing 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:

- Michael Abbott, Thorsten Altenkirch, and Neil Ghani,
*Representing Nested Inductive Types using W-types*(pdf)

Reference to Michael Abbott, Thorsten Altenkirch, and Neil Ghani, *Representing Nested Inductive Types using W-types*

Anonymous

]]>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.

]]>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…

]]>Added to *W-type* a section *Properties* with a pointer to Danielsson’s recent post.