Two-Level Type Theory and Applications