In this talk, I will present an extension of the Calculus of Constructions (the theory behind Coq) which allows to extend modularly the type system with new constructors and new inference rules. The idea is to define a translation between the new system and the original one, following the idea of Krivine and Miquel to study the translation of proofs induced by forcing. Our translation of forcing is is in fact an internalization in the type theory of the topos of presheaves of Birkedal et al.

I will then show how we can use this technique to extend the inductive types of Coq with negative occurrences. This will be used to formalize recent works on Kripke Logical Relations.