# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeFeb 8th 2010

Created W-type.

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeFeb 8th 2010

And a related query at pretopos.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeSep 22nd 2012

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

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeJan 9th 2014

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

• CommentRowNumber5.
• CommentAuthorTobyBartels
• CommentTimeJan 18th 2014
• (edited Jan 18th 2014)

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.

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

Anonymous

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeJul 25th 2019
• (edited Jul 25th 2019)

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:

• CommentRowNumber8.
• CommentAuthorspitters
• CommentTimeJul 25th 2019
Re #6. Thanks! I'll try to remember that.
• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeFeb 1st 2021

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeAug 13th 2021

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.

• CommentRowNumber11.
• CommentAuthorDavid_Corfield
• CommentTimeAug 13th 2021
• (edited Aug 13th 2021)

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.

• CommentRowNumber12.
• CommentAuthorMike Shulman
• CommentTimeAug 14th 2021

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

• CommentRowNumber13.
• CommentAuthorDavid_Corfield
• CommentTimeAug 14th 2021

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?

• CommentRowNumber14.
• CommentAuthorMike Shulman
• CommentTimeAug 15th 2021

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

• CommentRowNumber15.
• CommentAuthorMike Shulman
• CommentTimeAug 15th 2021

Thanks for pointing that out, have now resolved it.

• CommentRowNumber16.
• CommentAuthorUrs
• CommentTimeDec 31st 2022
• (edited Dec 31st 2022)

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

• CommentRowNumber17.
• CommentAuthorUrs
• CommentTimeJan 1st 2023
• (edited Jan 1st 2023)

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)$

• CommentRowNumber18.
• CommentAuthorUrs
• CommentTimeJan 1st 2023

fixed these bibitems:

• CommentRowNumber19.
• CommentAuthorUrs
• CommentTimeJan 1st 2023

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:

$\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} }$
• CommentRowNumber20.
• CommentAuthorUrs
• CommentTimeJan 1st 2023
• (edited Jan 1st 2023)

• CommentRowNumber21.
• CommentAuthorUrs
• CommentTimeJan 1st 2023

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

• CommentRowNumber22.
• CommentAuthorUrs
• CommentTimeJan 3rd 2023

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

(cf. nForum announcement here)