Skip to main content
2 of 2
Spelling in title
Neil Strickland
  • 56.9k
  • 7
  • 142
  • 262

Categorical semantics of W-types

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

Russell O'Connor
  • 1.4k
  • 1
  • 13
  • 15