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.

翻译：语义模型若满足完全可定义性，则模型中的每个语义元素都是某个证明或程序的指称。完全可定义性表明模型以高度精细的方式刻画了程序与证明。本文研究基于群胚上质子函子（bi）范畴的模型中的完全可定义性，该模型是关系模型的证明相关变体。尽管质子函子比关系复杂得多，但我们表明：将关系模型的思想进行直接推广，结合质子函子中稳定性的概念，即可完全刻画可定义的质子函子。更精确地说，所有稳定且全体的质子函子逻辑族均可由带MIX的乘法线性逻辑证明网定义。作为完全可定义性证明的一部分，我们证明了稳定性可作为正确性判据，这一结果本身具有独立的研究价值。