Is there a word I can say which will convey to type theorists that I am not thinking about types as propositions?

Background: as a category theorist, I am mostly interested in type theories as a language to express and prove things about the categories in which they naturally have semantics. E.g. typed lambda-calculus in cartesian closed categories, dependent type theory in locally cartesian closed categories, etc. Such categorical models can also be used when thinking of types as propositions, of course, but usually I am thinking of types (i.e. the objects in the categories in question) as more like sets (or groupoids or higher groupoids, sometimes). Sometimes the type theory even includes a separate notion of "proposition" which is interpreted by monomorphisms in the category, e.g. the geometric logic or "higher-order type theory" of toposes.

Of course, I can say "categorical type theory" to refer to the whole programme of semantics for type theories in categories. However, if I want to talk only about the type theory side of things, but I don't want people to start calling types "propositions" and terms "proofs," what can I say to convey the point of view I want to take?


Short answer: two-level type theory.

In type theory the idea that sets and propositions should be distinguished has been considered (of course). Peter Aczel and (then) his student Nicola Gambino proposed a "two-level" type theory in which $\mathsf{Set}$ and $\mathsf{Prop}$ are not identified. More recently, Giovanni Sambin and Emillia Maietti proposed a similar treatment (I am not sure I've got the best reference here, please fix it), which I think is more general, as it deals with other issues in type theory (intensionality vs. extensionality).

So, if you want to speak to type-theorists you should use the following buzzwords:

  • "I am not identifying $\mathsf{Set}$ and $\mathsf{Prop}$, you know, in the style of Aczel and Gambino.", or
  • "We consider a type theory with separate kinds for sets and propositions."
  • "We do not assume that propositions are identified with types."

If you want to be more specific, for example if your notion of proposition is that of a subobject, you can say:

  • "For me propositions are the proof-irrelevant types."

Some people know the idea of proof-irrelevance under the heading of "squash types" or "bracket "types". It is also worth mentioning that the Coq proof assistant has different kinds for sets and propositions.

  • $\begingroup$ Thanks, that's helpful. What if I want to talk about a type theory that doesn't include $\mathbf{Prop}$ at all, but whose types I don't want to regard as propositions? $\endgroup$ Oct 22 '10 at 18:02
  • $\begingroup$ Also, saying that "propositions are proof-irrelevant types" seems to imply that the terms of a general non-proof-irrelevant type are still thought of as "proofs," which is not what I want. But maybe that implication is only in my mind. $\endgroup$ Oct 22 '10 at 18:04
  • $\begingroup$ Well, since you're trying to say that you're not doing propositions, it's going to be hard not to mention propositions. But what are you worried about? If this is about LCCC's, just say "dependent type theory". Since there are many variations of DTT you will have to be quite precise about the details and then people will see that there is no $\mathsf{Prop}$. Type theorists are careful readers (should I say "formalists"?) and prefer to see too many details, not too few. $\endgroup$ Oct 22 '10 at 18:23
  • $\begingroup$ I don't want to not mention propositions, I just don't want to identify them with types. And as far as I can tell, the distinction isn't one that happens at a formal level, but rather at the level of informal discourse and intuition---the same formally defined DTT could be interpreted with types being propositions or not. $\endgroup$ Nov 7 '10 at 5:41

Since this question (which I just noticed) seems to be in reaction to my first response to your other question, let me explain again that response. The problem was not that I was implicitly assuming you are equating types with propositions. In any case typically it's the other way around: the propositions-as-types analogy says that propositions can be thought of as types, and type theorists often do so. So as Andrej said, if you want to reject this analogy it's hard to do so without mentioning propositions.

In this case I don't think the confusion had anything to do with propositions vs types. Rather, it was your assumption (in fairness, somewhat obvious on inspection of the question) that well-typed terms are distinct from typing derivations, so that we can speak of multiple derivations for the same well-typed term. Note this distinction makes just as much sense in logic as in type theory (distinguishing "proofs" and "proof verifications"), we just don't typically make it. And just as we don't have to make the distinction in logic, we don't have to make it in type theory.

If you want to make this assumption clear, I think it is best to just say, "I am distinguishing terms from typing derivations". As I alluded to in my second response, this distinction is sometimes called the "Curry view", and the lack of a distinction the "Church view"--but these are somewhat overloaded terms without universally accepted meanings (for example, sometimes people say "Church" and "Curry" for the presence or absence of type annotations in the syntax of lambda abstraction). The Pfenning paper I linked to sorts out some of these issues.

  • $\begingroup$ Thanks. I didn't intend this question to be only in reaction to your other response; I've had the same feeling in talking to type theorists before. But perhaps it is also due to my lack of understanding of what they mean by words. But even in your second response you seemed to be making a dichotomy which I didn't understand, one side of which was "directly identify types with propositions." $\endgroup$ Nov 7 '10 at 5:36
  • $\begingroup$ Actually I was trying to suggest precisely that it's a false dichotomy, albeit a frequently-made one under the label "Church vs Curry". I'm happy that you also see it as a false dichotomy! You should just be aware it exists, and that the word "type" does not have a fixed meaning in type theory. The reason I think your question here is misdirected is because accepting Curry-Howard does not mean settling on a particular meaning of "type" -- rather, it means taking advantage of the intuition that the word "type" has at least as many interpretations as the word "proposition", and vice versa. $\endgroup$ Nov 8 '10 at 15:01

"Term category of a hyperdoctrine."

The hyperdoctrine approach to categorical logic segregates the individuals (terms inhabiting types) in a category completely apart from the categories containing truth values and predicates (object-indexed truth values). In a hyperdoctrine nothing in the term category may be construed as a proposition -- those live elsewhere.

This contrasts with the approach of topoi, where there is an object of truth values $\Omega$ living in the same category as the type objects: propositions are morphisms into $\Omega$.

  • $\begingroup$ But one can just as easily think of the fiber categories of a hyperdoctrine as encoding propositions and proofs, and I think people often do, don't they? $\endgroup$ Nov 7 '10 at 5:38
  • $\begingroup$ Right, which is why you say TERM category (not FIBER category) when you want to prevent people from thinking about propositions and proofs. $\endgroup$
    – Adam
    Nov 7 '10 at 21:02
  • $\begingroup$ Oh, I misunderstood what you meant by "term category," sorry. Okay, that makes sense. $\endgroup$ Nov 9 '10 at 5:22
  • $\begingroup$ Although I would tend to regard a hyperdoctrine as more on the "semantics" side of things, along with lcccs and topoi, whereas I was more asking about the corresponding syntactic side. $\endgroup$ Nov 9 '10 at 5:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.