Homotopy type-theoretic interpretations of constructive set theories

DOI10.1017/S0960129519000148OpenAlexW2921141952MaRDI QIDQ5156772

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 theoryhomotopy type theorydependent type theorylogic-enriched type theory

Mathematics Subject Classification ID

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

Cites Work

• A minimalist two-level foundation for constructive mathematics
• 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
• The generalised type-theoretic interpretation of constructive set theory
• An experimental library of formalized Mathematics based on the univalent foundations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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