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$
1
  • $\begingroup$ The title of the question has a typo which should be fixed. $\endgroup$ Feb 7, 2012 at 17:04

2 Answers 2

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$
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$ 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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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