Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
fixed author name and added more hyperlinks for this item
added pointer (here and at calculus of constructions) to:
Added a reference to
added doi:10.1007/BF00176047
and copied the item also to the entries simple type theory and Alonzo Church
removing query box
I don't buy your argument that Prop must be treated specially; perhaps I don't understand what you're saying, but I'll pretend that I do. First, I don't see the relevance of your premise, that Prop makes things higher-order because it is a power type. You might as well say that 1 makes things higher-order because 1≅P0. What really makes things higher order is the ability to form arbitrary power types or function types, not the existence of one or two special cases. And second, I don't agree with the conclusion, that Prop can't participate in type operations. It's true that many type theories do treat Prop specially and forbid its participation in type operations, but allowing it to participate in first-order type operations like × and + is not going to make things higher order. Conversely, Prop≅1+1 in some type theories, in which case you can hardly stop it from participating in type operations! —Toby
Mike Shulman: This seems to be basically a dispute about the meaning of “higher-order”? To me, for something to be first-order, it should be interpretable in a Heyting category, which does not necessarily have a subobject classifier (though it does, as you point out, have a power object for 0). I also expect that the presence of Prop as a type is sufficient to make the Completeness Theorem fail, as described in the next paragraph. Probably “participate in type operations” is the wrong claim to be making, rather the claim should be something along the lines of Prop being a kind, rather than a type, i.e. we don’t have Prop:Type, or at least not Prop:Type0.
removing another query box
Quick comment: Even in internal type theory, one needs identity types to validate COSHEP. Type theory without identity types is very strange (the category of contexts may not have all pullbacks, and not every morphism need be a display morphism).
Mike Shulman: I’m not sure that that’s so strange. At least, not to the type theorists. (-: Categorically, I think of display maps as being fibrations in some model-category-type structure, which makes sense to me, although in semantics valued in an honest higher-category I would expect every morphism to be equivalent to a display morphism.
Actually, don’t you need extensional identity types in order to get all pullbacks and make every morphism display? I think intensional identity types just mean that you can factor every morphism through a display morphism which is “equivalent” in some sense, i.e. you have the identity type weak factorization system.
And I didn’t know that about COSHEP, why is that? Isn’t it true that all types are projective, at least in the propositions-as-types logic, since to assert that something exists is to give a construction of it? Or are you saying that you need identity types in order to even construct the category of setoids, since you need the category of types to have at least weak finite limits?
Toby: I mean that you need identity types in order to have the free functor from presets to sets that allows every type (preset) to be interpreted as a set. So every set is a quotient (in a sense) of a preset, and every preset is projective (in a sense), but it's not a projective set. We merely have that the free set on that preset is projective if it exists.
I really meant to work out a clean example of such a type theory on my personal web, but I never did (so you don't need to look there).
PS: You're right about the display maps; that part's not so strange. Maybe it's not strange at all, but Martin-Löf (at least) considers identity types indispensible (and they are, in his framework, for W-types to work).
moving section on extensional and intensional type theories from type theory article to dependent type theory article