The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective

DOI10.1016/J.ENTCS.2008.10.003zbMath1286.03029OpenAlexW2095650032WikidataQ62125660 ScholiaQ62125660MaRDI QIDQ5415629

Alexandre Buisse, Peter Dybjer

Publication date: 13 May 2014

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.10.003

zbMATH Keywords

Coqlocally Cartesian closed categoryE-categoryMartin-Löf intuitionistic type theory

Mathematics Subject Classification ID

Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Related Items (1)

Proof-relevance of families of setoids and identity in type theory

Uses Software

• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Locally cartesian closed categories and type theory
• Constructive mathematics and computer programming
• Fibered categories and the foundations of naive category theory
• Normalization and the Yoneda embedding
• Internal type theory
• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory

This page was built for publication: The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective