What types should not be

DOI10.1093/PHILMAT/NKZ014zbMATH Open1451.03009OpenAlexW2967397440MaRDI QIDQ5124673FDOQ5124673

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

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

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)

Cited In (4)

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

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)