Conservativity of equality reflection over intensional type theory

DOI10.1007/3-540-61780-9_68zbMath1434.03038OpenAlexW1821509023MaRDI QIDQ4647577

Martin Hofmann

Publication date: 15 January 2019

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61780-9_68

zbMATH Keywords

type theoryidentity typeelimination rulefunctional extensionalitycanonical element

Mathematics Subject Classification ID

Type theory (03B38)

Related Items (7)

On generalized algebraic theories and categories with families ⋮ The compatibility of the minimalist foundation with homotopy type theory ⋮ Indexed containers ⋮ Constructing a universe for the setoid model ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Pointers in Recursion: Exploring the Tropics ⋮ On the strength of dependent products in the type theory of Martin-Löf

Cites Work

• Internal type theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Conservativity of equality reflection over intensional type theory