What do I call type theory without Curry-Howard? - MathOverflow

What do I call type theory without Curry-Howard?

2010-10-22T02:34:30Z

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?

Answer by Andrej Bauer for What do I call type theory without Curry-Howard?

2010-10-22T06:13:32Z

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.

Answer by Noam Zeilberger for What do I call type theory without Curry-Howard?

2010-11-03T16:27:18Z

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.

Answer by Adam for What do I call type theory without Curry-Howard?

2010-11-03T21:07:03Z

"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$.