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.
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
-
$\begingroup$ 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! $\endgroup$– CayleeAug 31, 2011 at 14:45
-
$\begingroup$ I expect there to be more interaction between the intensional aspects of a model and the W-types. For example, what can be said about the identity types of a W-type? Does it ever exceed the h-level of its constituent parts (the branching types)? $\endgroup$ Aug 31, 2011 at 15:11
-
$\begingroup$ @Andrej: Of course there are questions about how W-types interact with identity types in the intensional setting, but as far as the semantics is concerned this does not matter. The only way I can see that this could affect the semantics is if you have in mind a different notion of W-type from the usual one (e.g., requiring the existence of propositional equalities instead of definitional equalities in the conversion rule, or something along these lines). $\endgroup$ Aug 31, 2011 at 18:03
-
1$\begingroup$ @Caylee: What I have in mind are the semantics of type theory which are a bit more general than the LCCC semantics that one sometimes first encounters. For this I would look at the books by Thomas Streicher ("Semantics of Type Theory") and Bart Jacobs ("Categorical Logic and Type Theory") on semantics of type theory. There are also some papers by Andy Pitts ("Categorical logic") and Martin Hofmann ("Syntax and semantics of dependent types") on these matters which I highly recommend. $\endgroup$ Aug 31, 2011 at 18:13