AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY
DOI10.1002/MALQ.19920380118zbMATH Open0798.03059OpenAlexW2071971451MaRDI QIDQ4295233FDOQ4295233
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
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
constructive type theoryintensional equalityelementary topos theorycategorical semantics of typesequality of types
Categorical logic, topoi (03G30) Topoi (18B25) Second- and higher-order arithmetic and fragments (03F35)
Cited In (12)
- Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types
- Three extensional models of type theory
- The interpretation of intuitionistic type theory in locally Cartesian closed categories -- an intuitionistic perspective
- Martin Hofmann’s contributions to type theory: Groupoids and univalence
- Characterizing the interpretation of set theory in Martin-Löf type theory
- Categorical and algebraic aspects of Martin-Löf type theory
- Toposes and intuitionistic theories of types
- An interpretation of Martin-Löf's type theory in a type-free theory of propositions
- What is the world of mathematics?
- Interpreting descriptions in intensional type theory
- Title not available (Why is that?)
- On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
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)
