Russian Constructivism in a Prefascist Theory
Pierre-Marie Pédrot · 2020
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.