arXiv:1703.03007math.CT
Homotopy type theory: the logic of space
HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.
Abstract
This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book "New Spaces for Mathematics and Physics" (ed. Gabriel Catren and Mathieu Anel).