Abstract. In this note we show that Friedman's syntactic translation for intuitionistic logical systems can be carried over to Martin-Löf's type theory, including universes provided some restrictions are made. Using this translation we show that the theory is closed under a higher type version of Markov's rule.
Erik Palmgren, March 9, 1999.