What types should not be

DOI10.1093/PHILMAT/NKZ014MaRDI QIDQ5124673zbMATH OpenOpenAlexFDO

Authors Bruno Bentzen

Publication date 30 September 2020

Published in Philosophia Mathematica (Search for Journal in Brave)

Full work available at URL http://philsci-archive.pitt.edu/18992/1/bentzen2020types.pdf

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)

Recommendations

• Type theory and homotopy
• A meaning explanation for HoTT
• Homotopy Type Theory
• Introduction -- from type theory and homotopy theory to univalent foundations
• Identity in homotopy type theory. II: The conceptual and philosophical status of identity in HoTT

Cited in

(4)

• Spiritus asper versus lambda: on the nature of functional abstraction
• Representation and Spacetime: The Hole Argument Revisited
• Substitution and Propositional Proof Complexity
• Univalence and ontic structuralism

This page was built for publication: What types should not be

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