Extensional concepts in intensional type theory, revisited
Logic
2025-12-23 v2 Logic in Computer Science
Category 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.
Cite
@article{arxiv.2310.05706,
title = {Extensional concepts in intensional type theory, revisited},
author = {Chris Kapulkin and Yufeng Li},
journal= {arXiv preprint arXiv:2310.05706},
year = {2025}
}
Comments
version accepted for publication