This no-problem session is essentially a reading report for paper McTT: A Verified Kernel for a Proof Assistant. I will introduce induction-recursion, which is unsupported by Rocq, and its usage in previous NbE-based formalizations of MLTT. Then I’ll discuss the technique proposed in the paper to workaround this limitation by taking advantage of the impredicativity of the Prop sort.

I didn’t know Shengyi is working on this project until the seminar.