  G\"odel's Dialectica interpretation was designed to obtain a relative
consistency proof for Heyting arithmetic, to be used in conjunction with the
double negation interpretation to obtain the consistency of Peano arithmetic.
In recent years, proof theoretic transformations (so-called proof
interpretations) that are based on G\"odel's Dialectica interpretation have
been used systematically to extract new content from proofs and so the
interpretation has found relevant applications in several areas of mathematics
and computer science. Following our previous work on G\"odel fibrations, we
present a (hyper)doctrine characterisation of the Dialectica which corresponds
exactly to the logical description of the interpretation. To show that we
derive in the category theory the soundness of the interpretation of the
implication connective, as expounded on by Spector and Troelstra. This requires
extra logical principles, going beyond intuitionistic logic, Markov's Principle
(MP) and the Independence of Premise (IP) principle, as well as some choice. We
show how these principles are satisfied in the categorical setting,
establishing a tight (internal language) correspondence between the logical
system and the categorical framework. This tight correspondence should come
handy not only when discussing the applications of the Dialectica already
known, like its use to extract computational content from (some) classical
theorems (proof mining), its use to help to model specific abstract machines,
etc. but also to help devise new applications.
