AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY

DOI10.1002/MALQ.19920380118MaRDI QIDQ4295233zbMATH OpenOpenAlexFDO

Authors Anne Preller

Publication date 3 November 1994

Published in Mathematical Logic Quarterly (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1002/malq.19920380118

zbMATH Keywords

constructive type theoryintensional equalityelementary topos theorycategorical semantics of typesequality of types

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• Toposes and intuitionistic theories of types
• scientific article; zbMATH DE number 4187810
• scientific article; zbMATH DE number 2079044
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Modular correspondence between dependent type theories and categories including pretopoi and topoi

Cited in

(12)

• scientific article; zbMATH DE number 1302058 (Why is no real title available?)
• Three extensional models of type theory
• Martin Hofmann’s contributions to type theory: Groupoids and univalence
• The interpretation of intuitionistic type theory in locally Cartesian closed categories -- an intuitionistic perspective
• Categorical and algebraic aspects of Martin-Löf type theory
• Interpreting descriptions in intensional type theory
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• Toposes and intuitionistic theories of types
• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
• What is the world of mathematics?

This page was built for publication: AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4295233)