Viliam comments on Basic building blocks of dependent type theory