# 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