Univalent Foundations and the UniMath Library

DOI10.1007/978-3-030-15655-8_8zbMath1528.03104arXiv1710.02723OpenAlexW2762612567MaRDI QIDQ6075426

Anthony Bordg

Publication date: 20 September 2023

Published in: Synthese Library (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45) Digital mathematics libraries and repositories (68V35)

Cites Work

• Isomorphism is equality
• Nicholas Bourbaki, collective mathematician. An interview with Claude Chevalley
• The unreasonable effectiveness of mathematics in the natural sciences. Richard courant lecture in mathematical sciences delivered at New York University, May 11, 1959
• Homotopy Type Theory: Univalent Foundations of Mathematics
• An experimental library of formalized Mathematics based on the univalent foundations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Univalent Foundations and the UniMath Library