The Dialectica categories

Valeria Correa Vaz de Paiva
This work consists of two main parts. The first one, which gives it its name, presents an internal categorical version of Gödel’s “Dialectica interpretation” of higher-order arithmetic. The idea is to analyse the Dialectica interpretation using a cetegory DC where objects are relations on objects of a basic category C and maps are pairs of maps of C satisfying a pullback condition. If C is finitely complete, DC exists and has a very natural symmetric...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.