A meaning explanation for HoTT

DOI10.1007/s11229-018-02052-1zbMath1475.03055OpenAlexW2590129007WikidataQ128646999 ScholiaQ128646999MaRDI QIDQ2054122

Dimitris Tsementzis

Publication date: 1 December 2021

Published in: Synthese (Search for Journal in Brave)

Full work available at URL: http://philsci-archive.pitt.edu/12824/1/A.Meaning.Explanation.for.HoTT.pdf

zbMATH Keywords

set theoryhomotopy type theoryunivalent foundationsmeaning explanation

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Related Items (1)

Models of HoTT and the Constructive View of Theories

Uses Software

• UniMath
• cubicaltt
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Generalized algebraic theories and contextual categories
• Univalent foundations as structuralist foundations
• Mathematical forms and forms of mathematics: leaving the shores of extensional mathematics
• Homotopy type theory and Voevodsky’s univalent foundations
• Identity in Homotopy Type Theory, Part I: The Justification of Path Induction
• Homotopy theoretic models of identity types
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• An introduction to univalent foundations for mathematicians
• Category Theory as an Autonomous Foundation
• Structuralism, Invariance, and Univalence
• Program Testing and the Meaning Explanations of Intuitionistic Type Theory
• THE CLASSICAL CONTINUUM WITHOUT POINTS
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: A meaning explanation for HoTT