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

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. 


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

