Homotopy type-theoretic interpretations of constructive set theories

DOI10.1017/S0960129519000148MaRDI QIDQ5156772zbMATH OpenOpenAlexFDO

Authors Cesare Gallozzi

Publication date 11 October 2021

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

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

zbMATH Keywords

constructive set theorydependent type theoryhomotopy type theorylogic-enriched type theory

Mathematics Subject Classification ID

Type theory (03B38) Nonclassical and second-order set theories (03E70) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Recommendations

• Characterizing the interpretation of set theory in Martin-Löf type theory
• The generalised type-theoretic interpretation of constructive set theory
• Functional interpretation of Aczel's constructive set theory
• Heyting-valued interpretations for constructive set theory
• scientific article; zbMATH DE number 1420782

Cites work

• A minimalist two-level foundation for constructive mathematics
• An experimental library of formalized mathematics based on the univalent foundations
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Constructive set theory
• From multisets to sets in homotopy type theory
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3839951 (Why is no real title available?)
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 2085163 (Why is no real title available?)
• The generalised type-theoretic interpretation of constructive set theory

Cited in

(4)

• scientific article; zbMATH DE number 1104367 (Why is no real title available?)
• Towards Constructive Homological Algebra in Type Theory
• scientific article; zbMATH DE number 4187810 (Why is no real title available?)
• Interpretation of inaccessible sets in Martin-Löf type theory with one Mahlo universe

This page was built for publication: Homotopy type-theoretic interpretations of constructive set theories

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