Homotopy type theory and Voevodsky’s univalent foundations

DOI10.1090/S0273-0979-2014-01456-9zbMath1432.03019arXiv1210.5658MaRDI QIDQ2933829

Álvaro Pelayo, Michael A. Warren

Publication date: 8 December 2014

Published in: Bulletin of the American Mathematical Society (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1210.5658

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

03G30: Categorical logic, topoi

55U35: Abstract and axiomatic homotopy theory in algebraic topology

55U40: Topological categories, foundations of homotopy theory

03B38: Type theory

18N45: Categories of fibrations, relations to (K)-theory, relations to type theory

Uses Software

• Coq