1 paper
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard +2
We present an extensive mechanization of the meta-theory of Martin-Löf Type Theory (MLTT) in the Coq proof assistant. Our development builds on pre-existing work in Agda to show no…