UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY

DOI10.1017/S1755020316000460WikidataQ127483562 ScholiaQ127483562MaRDI QIDQ5241229

James Ladyman, Stuart Presnell

Publication date: 30 October 2019

Published in: The Review of Symbolic Logic (Search for Journal in Brave)

zbMATH Keywords

equivalenceunivalenceisomorphismuniverseshomotopy type theorystructuralismawodey

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX)

Related Items (2)

Naive cubical type theory ⋮ Representation and Spacetime: The Hole Argument Revisited

Uses Software

• HoTT
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Some proposals for reviving the philosophy of mathematics
• Identity in Homotopy Type Theory, Part I: The Justification of Path Induction
• Voevodsky’s Univalence Axiom in Homotopy Type Theory
• Does Homotopy Type Theory Provide a Foundation for Mathematics?
• Identity in Homotopy Type Theory: Part II, The Conceptual and Philosophical Status of Identity in HoTT
• Structuralism, Invariance, and Univalence
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY