In recent work, Michael Lambert and I showed that cartesian double theories and their models, which are span-valued cartesian lax functors, provide a unifying framework for doctrines, at least up to a certain level in the hierarchy of categorical logic (Lambert and Patterson 2023). We considered two kinds of morphisms between lax double functors, namely lax natural transformations1 and modules, and showed that they form the arrows and proarrows of a (virtual) double category. Yet there is a third known kind of morphism between lax functors, transformations whose components are proarrows rather than arrows. We did not consider such “protransformations” between models of double theories. Are they good for anything? The answer, it turns out, is yes!
This is a companion discussion topic for the original entry at https://topos.site/blog/2023-10-20-retrotransformations/