Conservativity of equality reflection over intensional type theory
From MaRDI portal
Publication:4647577
Recommendations
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)