Conservativity of equality reflection over intensional type theory

1996/01/01 by Martin Hofmann · 1 voice · 1 citation
Computer Science · Mathematics · #Advanced Algebra and Logic #Advanced Topology and Set Theory

paper · doi:10.1007/3-540-61780-9_68

crossref issued 1996/01/01 · crossref published 1996/01/01 · crossref published-print 1996/01/01 · openalex publication_date 1996/01/01 · crossref published-online 2005/06/07 · crossref created 2012/02/26 · crossref deposited 2020/11/17 · openalex created_date 2025/10/10 · crossref indexed 2026/04/16 · openalex updated_date 2026/07/29

Cited by

• Relative induction principles for type theories

Discussions

• In fact, there is a result of Hoffmann which I was not aware of but is probably standard: extensional MLTT is conservative over (intensional) MLTT + UIP + funext. doi.org/10.1007/3-54... [bsky, 1 points, 0 comments]