Staged Compilation With Two-Level Type Theory