# What are categorical models of W-types in intensional type theory?

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.

-

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.
Huh - perhaps I'm coming at this from the wrong direction in the literature. So the semantics in the extensional case, as I learned it, is given by certain equivalence classes of functors on the category of types. For the extensional theory interpreted in LCCCs these are all of the form $\Sigma a:A. Ba \rightarrow X$ for some choice of types A & B. It sounds like there's a more general interpretation of W-types from the fibred perspective that I simply didn't know. Could you name a good place to start digging further into the kind of models you're talking about? Thanks! –  Caylee Aug 31 '11 at 14:45