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

canonical elementelimination rulefunctional extensionalityidentity typetype theory

Mathematics Subject Classification ID

Type theory (03B38)

Recommendations

• Extensional constructs in intensional type theory
• Extensionality of ^*
• 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

(17)

• On the strength of dependent products in the type theory of Martin-Löf
• Constructing a universe for the setoid model
• Three extensional models of type theory
• Extensional constructs in intensional type theory
• On generalized algebraic theories and categories with families
• Pointers in Recursion: Exploring the Tropics
• Proof theory of constructive systems: inductive types and univalence
• Extensionality of ^*
• Indexed containers
• Elimination of extensionality in Martin-Löf type theory
• The compatibility of the minimalist foundation with homotopy type theory
• From rewrite rules to axioms in the \(\lambda \varPi \)-calculus modulo theory
• Equiconsistency of the minimalist foundation with its classical version
• Lean4Less: eliminating definitional equalities from Lean via an extensional-to-intensional translation
• A syntax for mutual inductive families
• Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
• A 2-categorical approach to the semantics of dependent type theory with computation axioms

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)