This is a recent Agda formalization of a 2006 paper by Martin-Löf. Comments