I'm familiar with container functors and older work by Dybjer on categorical models for W-types in the extensional theory, but I was looking for some similar semantics in the intensional case.
Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)
|
4
1
|
|
|
|
|
4
|
Unless I've not understood your question correctly (sometimes people mean different things by the distinction between intensional and extensional), then I think the answer is: the semantics for W-types in intensional type theory are exactly the same as the semantics for W-types in extensional type theory. A model of type theory (comprehension category, category with attributes, et cetera) is essentially just a Grothendieck fibration $p:E\to B$ which comes equipped with certain structure. Being a model of W-types just means that $p$ comes equipped with certain extra structure. As I understand it, the difference between intensional and extensional type theory has to do with which axioms are satisfied by the identity types. (In terms of $p$ this is just whether it is equipped with one or another kind of structure for interpreting identity types.) Whether or not you are able to interpret W-types is again simply a question of whether $p$ has a further kind of additional structure and is a prior independent of which kind of identity types $p$ is able to interpret. In practical terms, what this means is that the question of whether your model supports the interpretation of W-types has everything to do with your fibration $p$ and formulated in this way the question is completely independent of whether the model is intensional or extensional. E.g., if your fibration $p$ comes from something like a class of display maps and you want to interpret W-types as initial algebras for polynomial endofunctors, then you will need to verify that these initial algebras land in the class of display maps. |
||||||||||||||
|

