Skolem, G\"odel, and Hilbert fibrations

TL;DR

This paper characterizes generalized Dialectica fibrations and introduces Hilbert fibrations, providing a categorical framework for understanding dependency, quantifiers, and proof-theoretic operators in logic and type theory.

Contribution

It offers a new internal characterization of dependent Dialectica fibrations and generalizes G"odel fibrations to the dependent setting, also introducing Hilbert fibrations.

Findings

Characterization of dependent Dialectica fibrations as iterated completions.

Generalization of G"odel fibrations to arbitrary display maps.

Introduction of Hilbert fibrations for proof-theoretic operators.

Abstract

Grothendieck fibrations are fundamental in capturing the concept of dependency, notably in categorical semantics of type theory and programming languages. A relevant instance are Dialectica fibrations which generalise G\"odel's Dialectica proof interpretation and have been widely studied in recent years. We characterise when a given fibration is a generalised, dependent Dialectica fibration, namely an iterated completion of a fibration by dependent products and sums (along a given class of display maps). From a technical perspective, we complement the work of Hofstra on Dialectica fibrations by an internal viewpoint, categorifying the classical notion of quantifier-freeness. We also generalise both Hofstra's and Trotta et al.'s work on G\"odel fibrations to the dependent case, replacing the class of cartesian projections in the base category by arbitrary display maps. We discuss how this recovers a range of relevant examples in categorical logic and proof theory. Moreover, as another instance, we introduce Hilbert fibrations, providing a categorical understanding of Hilbert's $\epsilon$- and $\tau$-operators well-known from proof theory.