Syntax of dependent type theories An Agda formalization of the raw syntax for dependent type theories.