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)?
Categorical semantics of W-types
Russell O'Connor
- 1.4k
- 1
- 13
- 15