lucidity vs ludicity, and translating one esoteric language into a slightly less esoteric one

One of the things I often wonder about is how to say things that are intelligible. Too frequently, I lapse into jargon─sometimes even on-the-spot-invented jargon─and only realize this after the damage has been done. An example: the previous blog post, which was probably incomprehensible to all but...well, probably to all. I promise I will try hard to avoid doing this in the future.

But on the topic of making things less inscrutable─and not on the topic of Girard!, though keep your eyes on the Girard Reading Group Wiki─another thing I've been thinking about is how to translate Martin-Löf's "judgment vs proposition" distinction (as spelled out in the Siena Lectures) into the language of category theory. At first, the judgment vs proposition distinction may seem pedantic: okay, one can distinguish between a well-formed proposition "A" and the assertion that it is true "A true"...but so what? Well, the distinction helps get dependent type theory off the ground, since well-formedness is defined mutually with truth (the dependent quantifier ∏x:A.B is a well-formed proposition if and only if A is well-formed and B is well-formed under the assumption x:A). More mundanely, it is obvious that a separate notion of judgment is useful if we want to refute propositions as well as assert them, using the judgment "A false" in addition to "A true".

Well, this is actually not quite so obvious. Why not just assert ¬A? For a philosophical explanation of why not, Greg Restall's essay "Multiple Conclusions" is a nice read. From a proof/type-theoretic perspective, the reason why not to identify "A false" with "¬A " is that we need the separate judgment in order to obtain "good compositionality" principles─this is an informal but very general law gleaned by Frank Pfenning and collaborators over years of refining the "judgmental method", to which the paper "A judgmental reconstruction of modal logic" probably serves as the most complete introduction. Unfortunately, though, my impression is that these principles are still not very widely accepted or understood.

I think part of the problem is the seemingly obscure philosophical origins of the judgmental method (although its application is practically motivated), and so what I would like is a translation guide into the language of category theory (an order of magnitude less obscure, though granted still sometimes considered esoteric) . I think there must be such a translation, since the whole point of the judgmental method (at least in my mind) is obtaining compositionality principles.

Does anyone know if the judgment vs proposition distinction has been explored before in category theory? As a simple example of a system with two judgments that should be possible to explain categorically, I propose the bidirectional lambda calculus with implication and conjunction (described in Section 3.1 here).