Set-theoretical models of various type theories (up to an extensional version of the Calculus of Inductive Constructions), aiming at proving logical consistency and strong normalization
Hi @barras, I started to port this development to 8.7 which is less easy than I thought. Did you already did some work in this direction, or shall I continue without risking to make twice the same job?
(Initially, I wanted to understand how far we can build the von Neumann hierarchy in pure CIC. We should at least be able to go up to V_ε^CK or are my intuitions wrong?)