  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.
