Conservativity of equality reflection over intensional type theory

DOI10.1007/3-540-61780-9_68zbMATH Open1434.03038OpenAlexW1821509023MaRDI QIDQ4647577FDOQ4647577

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

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

zbMATH Keywords

type theoryidentity typeelimination rulefunctional extensionalitycanonical element

Mathematics Subject Classification ID

Type theory (03B38)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Internal type theory
• Title not available (Why is that?)

Cited In (12)

• Three extensional models of type theory
• Proof theory of constructive systems: inductive types and univalence
• Constructing a universe for the setoid model
• 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)