Homotopy type-theoretic interpretations of constructive set theories

DOI10.1017/S0960129519000148OpenAlexW2921141952MaRDI QIDQ5156772FDOQ5156772

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

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
• Publication:4944846

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

• Title not available (Why is that?)
• Constructive set theory
• Homotopy type theory. Univalent foundations of mathematics
• A minimalist two-level foundation for constructive mathematics
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The generalised type-theoretic interpretation of constructive set theory
• From multisets to sets in homotopy type theory
• An experimental library of formalized mathematics based on the univalent foundations

Cited In (3)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Towards Constructive Homological Algebra in Type Theory

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)