Extensional concepts in intensional type theory, revisited

Chris Kapulkin, Yufeng Li

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…