Godel's Dialectica has been introduced and developed as a logical transformation. Only recently has it been related with the, a priori unrelated, notion of differentiation: we can now read it as a differentiable program transformation. Building on that, we formulate the relation between these two notions categorically, in the framework of differential categories. Moreover, we study the relation between differential categories and Dialectica categories. We do this by taking the point of view of fibrations and (dependent) lenses, which allows us to keep a geometrical intuition in mind by considering reverse tangent categories. The viewpoint we propose opens many interesting further developments.

翻译：哥德尔的Dialectica最初是作为一种逻辑变换被提出和发展的。直到最近，它才与先验无关的微分概念建立联系：我们现在可以将其解读为一种可微分的程序变换。基于此，我们从范畴论的角度——在微分范畴的框架下——对这两个概念之间的关系进行了形式化表述。此外，我们研究了微分范畴与Dialectica范畴之间的关联。我们通过采用纤维化与（依赖）透镜的视角来实现这一研究，这一视角使我们能够借助考虑逆向切范畴来保持几何直观性。我们所提出的观点为许多有趣的后续发展开辟了道路。