Full Definability in a Profunctorial Model
Abstract
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.
Cite
@article{arxiv.2604.26829,
title = {Full Definability in a Profunctorial Model},
author = {Takeshi Tsukada and Kazuyuki Asada and Kengo Hirata},
journal= {arXiv preprint arXiv:2604.26829},
year = {2026}
}