You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Leopold Schlicht (Aug 12 2021 at 09:14):The HoTT book (specifically chapter 5) acts like there is a concept of "inductive type", of which the notion of a "W-type" is a special case:
So far, we have been discussing only particular inductive types: 0, 1, 2, N, coproducts, products, Σ-types, W-types, etc.
What would be an example of an inductive type that is not a W-type? I always thought of "W-type" as an already quite general notion of the idea of an "inductive type".