# The missing category of (constructive) logic

It is well-known that the types in a given programming language form a category, based on Set, with their functions as morphisms.

It is also well-known that any program is basically a proof in constructive logic - the result is called in Curry–Howard correspondence and it is used in theorem prover software like Coq and Agda.

Doesn't, then, constructive logic form a category, in its own right? The objects are logical assertions, the morphisms are implications and True and False are, as in Coq, the initial and terminal object? And if yes, why isn't that category defined anywhere?

I am asking this is because it seems weird to me that many people talk about the connection between logic and Category theory, but as far as I know no one formalizes it.

• Yes, you can do that if you want. Do you have any application in mind? Are you just asking for he name of this "missing" category (which I don't know)? – realdonaldtrump Nov 9 '17 at 7:55
• My implicit question is "why isn't that category defined anywhere?" – Bobby Marinoff Nov 9 '17 at 8:19
• I think that it will serve as a great example of a "categorization" of a well-known concept (I think that the main issue with teaching CT is that there are too few examples). – Bobby Marinoff Nov 9 '17 at 8:21
• Regarding the first sentence: math.andrej.com/2016/08/06/hask-is-not-a-category – Dap Nov 9 '17 at 9:06
• OK, I know that Haskell is not a real category, due to the existence of bottom values, but I think that a subset of Haskell is a category. Am I wrong? And is this why logic also can't be thought as a category? – Bobby Marinoff Nov 9 '17 at 10:06

• So my category would be called, something like Con(Intui) in which an object would be a set of assertions, for example (A -> B, A) and a morphism would convert one set of assertions to another, like (A -> B, A) -> (A). Right? – Bobby Marinoff Nov 10 '17 at 8:46