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

$\endgroup$
  • $\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$

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.

$\endgroup$
  • 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 Feb 7 '12 at 21:37
3
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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