Extensional concepts in intensional type theory, revisited

TL;DR

This paper provides a direct proof of Morita equivalence between extensional and certain extended intensional type theories, clarifying their conceptual relationship and foundational properties.

Contribution

It offers a new, direct proof of Morita equivalence for extensional and extended intensional type theories, revisiting a classic result with a modern approach.

Findings

Establishes Morita equivalence between extensional and extended intensional type theories

Clarifies the relationship between extensionality principles and intensional type theory

Provides a direct proof approach for foundational equivalences in type theory

Abstract

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.