MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Jacob's book titled "Categorical Logic and Type Theory" gives a nice description of Π and Σ types as adjunctions to substitution functors induced by display maps. Is there a similar categorical description of W-types (and maybe M-types while we are at it)?

share|cite|improve this question
The title of the question has a typo which should be fixed. – Michael A Warren Feb 7 '12 at 17:04
up vote 12 down vote accepted

The categorical semantics of W-types, as initial algebras, have been studied in the following paper of Moerdijk and Palmgren: "Wellfounded trees in categories", Annals of Pure and Applied Logic 104(2000), 189 - 218.

share|cite|improve this answer
And for M-types (as terminal coalgebras) there is the dual paper "Non-well-founded trees in categories" by van den Berg and de Marchi, APAL 146 (2007) 40–59. – Mike Shulman Feb 7 '12 at 21:37

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.