Russian Constructivism in a Prefascist Theory

The results from this paper are twofold. First, we give a purely syntactic presheaf model of CIC. Contrarily to similar endeavours, this variant both preserves conversion and interprets full dependent elimination.

Using a particular instance of this model, we show how to extend CIC with Markov's principle, while preserving all good meta-theoretical properties like canonicity and decidability of type-checking. The resulting construction can be seen as a synthetic presentation of Coquand-Hofmann's syntactic model of PRA 𝜔 + MP as the composition of Pédrot-Tabareau's exceptional model with our presheaf interpretation.