What are categorical models of W-types in intensional type theory? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-24T12:04:28Z http://mathoverflow.net/feeds/question/74119 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/74119/what-are-categorical-models-of-w-types-in-intensional-type-theory What are categorical models of W-types in intensional type theory? Caylee 2011-08-31T01:55:28Z 2011-08-31T12:43:17Z <p>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.</p> http://mathoverflow.net/questions/74119/what-are-categorical-models-of-w-types-in-intensional-type-theory/74157#74157 Answer by Michael A Warren for What are categorical models of W-types in intensional type theory? Michael A Warren 2011-08-31T12:43:17Z 2011-08-31T12:43:17Z <p>Unless I've not understood your question correctly (sometimes people mean different things by the distinction between <em>intensional</em> and <em>extensional</em>), 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.</p> <p>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 <em>a prior</em> independent of which kind of identity types $p$ is able to interpret. </p> <p>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.</p>