The bridge between logic and geometry - motivating the work of Olivia Caramello

There are several beautiful and profound foundational papers (many from the 1970s) on inituitionistic higher-order logic within the framework of topos theory. Papers by Lawvere, D. Scott, M. Fourman, G. E. Reyes and others which focus on the philosophical aspects of formal presentations of higher order intuitionistic logic inspired by the structure of elementary topoi: partial domains, sorts and types, definite descriptions, definability, non-classical truth values, the interpretation of bounded quantifiers, the axiom of infinity (NNOs), the Russell-Prawitz translation (Scott claims to have discovered this in the 50s), etc.
There is an elegant Hilbert-style formal presentation of intuitionistic higher-order logic employed by Fourman in his paper in the Handbook of Mathematical Logic.

In our paper "Hegel and Modern Topology" we proposed an interpretation of the the Logic of Concept wherein the stages of Subjective Concept and Objective Concept and their integration are interpreted in terms of the duality between theories and models (understood as a geometrically inspired category theoretic framework for general systems theory) and the problem of finding a bridge between the two - something which partakes of the essence of both, perhaps in the style of algebraic logic.

In the paper by Fourman he uses only the most rudimentary notions of category theory. The main result is that any (elementary) topos is equivalent (via a logical morphism) to the topos of a definitionally complete theory E(T) and that any theory T gives rise to a topos E(T). Thus the objects E(T) -  bearing in mind their universal property (theorem 8.9 in the paper by Fourman) - would seem to be a candidate for a bridge between theories and models. E(T) classifies models of T: there is a correspondence between models M of T and logical morphisms E(T) -> M.

But Fourman remarks (he terms it an "embarassement") that this still does not constitute a bridge between (higher-order) logic and geometry (i.e. Objective Concept), between theories and Grothendieck topoi and their geometric morphisms. Fourman mentions a paper by Reyes in which Grothendieck topoi are described in terms of adding to Set a "generic model" for a possibly infinitary first-order theory.