Conservativity of equality reflection over intensional type theory

DOI10.1007/3-540-61780-9_68MaRDI QIDQ4647577zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Extensional constructs in intensional type theory
• Extensionality of \(\lambda^*\)
• scientific article; zbMATH DE number 1746890
• On the strength of dependent products in the type theory of Martin-Löf
• scientific article; zbMATH DE number 1302059

Cites work

• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3568670 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• Internal type theory

Cited in

(12)

• Three extensional models of type theory
• Constructing a universe for the setoid model
• Proof theory of constructive systems: inductive types and univalence
• From rewrite rules to axioms in the \(\lambda \varPi \)-calculus modulo theory
• On the strength of dependent products in the type theory of Martin-Löf
• Indexed containers
• Extensionality of \(\lambda^*\)
• Equiconsistency of the minimalist foundation with its classical version
• On generalized algebraic theories and categories with families
• The compatibility of the minimalist foundation with homotopy type theory
• Pointers in Recursion: Exploring the Tropics
• Elimination of extensionality in Martin-Löf type theory

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4647577)