# Categorical Brouwer-Heyting-Kolmogorov interpretation

Let $\mathcal{L}$ be the language of intuitionistic propositional logic generated by some atomic propositions $t_1, t_2, \ldots$. The Lindenbaum–Tarski algebra of $\mathcal{L}$ can be regarded as a bicartesian closed category in which there is an arrow $p \to q$ if and only if there is a proof of $q$ assuming $p$. Unfortunately it is a somewhat dull category, as there is at most one arrow between any two objects.

Question. Is there a categorification of the Lindenbaum–Tarski algebra which enables a category-theoretic form of the Brouwer–Heyting–Kolmogorov interpretation of intuitionistic propositional logic? In particular,

• Objects should be propositions.
• Arrows should be (equivalence classes) of proofs.
• The coproduct should be disjoint, at least for the coproduct of two distinct atomic propositions.
• The terminal object should be indecomposable, so that the disjunction property is validated (i.e. an arrow $\top \to p \lor q$ is either an arrow $\top \to p$ or an arrow $\top \to q$).

It feels like the free bicartesian closed category generated by the atomic propositions is the most likely candidate, and it can be concretised by the Yoneda embedding into the presheaf topos: then we would have a genuine BHK interpretation, i.e. interpreting a proposition as the ‘set’ of its proofs. This has probably been well-studied, in which case I would appreciate any references to the literature.

-
–  Qiaochu Yuan Nov 29 '11 at 23:53

I don't have it with me, and I can't recall the exact details, but I'm pretty sure Lambek & Scott's Introduction to Higher-Order Categorical Logic (link) is what you're looking for. In particular, they prove the equivalence between cartesian closed categories and simply-typed $\lambda$-calculi (so you get the Curry--Howard correspondence for free!).
In Part I, section 11, Lambek and Scott construct the cartesian closed category generated by a typed λ-calculus, which I can believe is what I want, except on the wrong side of the Curry–Howard isomorphism. It's not clear to me that the terminal object $\top$ is indecomposable in this category though – they only prove the disjunction property in the context of toposes and type theory later in the book, via the Freyd cover. –  Zhen Lin Nov 30 '11 at 7:50