Welcome to MathOverflow

Question

7

1

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

edited Feb 7 2012 at 17:04

Neil Strickland
13.5k●1●28●66

asked Feb 7 2012 at 16:28

Russell O'Connor
829●6●11

The title of the question has a typo which should be fixed. – Michael A Warren Feb 7 2012 at 17:04

Michael A Warren · Accepted Answer · 2012-02-07 17:00:21Z UTC

9

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.

answered Feb 7 2012 at 17:00

Michael A Warren
465●2●5

2

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. – Mike Shulman Feb 7 2012 at 21:37

Ivanych · Answer 2 · 2012-02-08 03:33:18Z UTC

3

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

answered Feb 8 2012 at 3:33

Ivanych
31●1

Categorical semantics of W-types

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

2 Answers

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.