ANNA BUCALO a1, FURIO HONSELL a1, MARINO MICULAN a1, IVAN SCAGNETTO a1andMARTIN HOFFMAN a2 a1 Department of Mathematics and Computer Science, University of Udine, Italy email: miculan@dimi.uniud.it a2 Institut für Informatik, Ludwig-Maximilians-Universität, München, Germany
The Theory of Contexts is a type-theoretic axiomatization aiming to give a metalogical account of the fundamental notions of variable and context as they appear in Higher Order Abstract Syntax. In this paper, we prove that this theory is consistent by building a model based on functor
categories. By means of a suitable notion of forcing, we prove that this model validates Classical Higher Order Logic, the Theory of Contexts, and also (parametrised) structural induction and recursion
principles over contexts. Our approach, which we present in full detail, should also be useful for reasoning on other models based on functor categories. Moreover, the construction could also be adopted, and possibly generalized, for validating other theories of names and binders.
