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 Wtypes (and maybe Mtypes while we are at it)?
9

$\begingroup$ The title of the question has a typo which should be fixed. $\endgroup$ – Michael A Warren Feb 7 '12 at 17:04
12
$\begingroup$
$\endgroup$
The categorical semantics of Wtypes, 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.

2$\begingroup$ And for Mtypes (as terminal coalgebras) there is the dual paper "Nonwellfounded trees in categories" by van den Berg and de Marchi, APAL 146 (2007) 40–59. $\endgroup$ – Mike Shulman Feb 7 '12 at 21:37
3
$\begingroup$
$\endgroup$
Also, this may be helpfull — http://ncatlab.org/nlab/show/polynomial+functor http://ncatlab.org/nlab/show/Wtype