Revisiting a classic result from M. Hofmann's dissertation, we give a direct proof of Morita equivalence, in the sense of V. Isaev, between extensional type theory and intensional type theory extended by the principles of functional extensionality and of uniqueness of identity proofs.

翻译：重新审视M. Hofmann学位论文中的经典结果，我们根据V. Isaev的定义，直接证明了外延类型论与扩展了函数外延性和恒等证明唯一性原理的内涵类型论之间的森田等价性。