Elimination of extensionality in Martin-Löf type theory

DOI10.1007/3-540-58085-9_76zbMath1527.03009OpenAlexW2028419206MaRDI QIDQ6083693

No author found.

Publication date: 8 December 2023

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

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Type theory (03B38)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Comprehension categories and the semantics of type dependency
• Categorical logic and type theory
• Extensional Gödel functional interpretation. A consistency proof of classical analysis

This page was built for publication: Elimination of extensionality in Martin-Löf type theory