Full Definability in a Profunctorial Model
It provides a complete characterization of definable elements in a proof-relevant semantic model, extending results from the relational model to a more complex setting.
The paper proves that all logical families of stable and total profunctors are definable by proof-nets of multiplicative linear logic with MIX, establishing full definability in a profunctorial model despite the complexity of profunctors.
A semantic model enjoys full definability if every semantic element in the model is a denotation of some proof or program. Full definability indicates that the model captures programs and proofs in a highly detailed manner. This paper studies full definability in a model based on the (bi)category of profunctors on groupoids, which is a proof-relevant variant of the relational model. Despite the fact that a profunctor is far more complicated than a relation, we show that a rather straightforward application of the ideas for the relational model, together with the notion of stability in profunctors, provides a complete characterisation of definable profunctors. More precisely, all logical families of stable and total profunctors are definable by proof-nets of multiplicative linear logic with MIX. As a part of the full definability proof, we show that the stability serves as a correctness criterion, which we think is of independent interest.