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 to as it seemed rather bad style to have a category named with objects named , and .
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:
1 to 9 of 9