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)?
Take the 2minute tour
×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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 

