Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types

DOI10.1017/S0960129500001080zbMath0860.03044OpenAlexW2154119530MaRDI QIDQ4715672

Geneviève Simonet, Anne Preller

Publication date: 18 November 1996

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129500001080

zbMATH Keywords

functional completenesslocally Cartesian closed categoriesinterpretation of Martin-Löf's extensional type theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Fibered categories (18D30) Second- and higher-order arithmetic and fragments (03F35) Foundations, relations to logic and deductive systems (18A15)

Cites Work

• Unnamed Item
• Locally cartesian closed categories and type theory
• Fibered categories and the foundations of naive category theory
• AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY
• Functional completeness of cartesian categories

This page was built for publication: Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types