9
$\begingroup$

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

Improve this question
$\endgroup$
1
  • $\begingroup$ The title of the question has a typo which should be fixed. $\endgroup$
    – Michael A Warren
    Commented Feb 7, 2012 at 17:04

2 Answers 2

Reset to default
12
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ 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. $\endgroup$
    – Mike Shulman
    Commented Feb 7, 2012 at 21:37
3
$\begingroup$

Also, this may be helpfull — http://ncatlab.org/nlab/show/polynomial+functor http://ncatlab.org/nlab/show/W-type

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .