philip_b comments on Basic building blocks of dependent type theory