Voevodsky’s Univalence Axiom in Homotopy Type Theory

DOI10.1090/noti1043zbMath1337.03014arXiv1302.4731OpenAlexW2963991919WikidataQ114009917 ScholiaQ114009917MaRDI QIDQ3193040

Michael A. Warren, Álvaro Pelayo, Steven Awodey

Publication date: 14 October 2015

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

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

Mathematics Subject Classification ID

Topological categories, foundations of homotopy theory (55U40)

Related Items (6)

Homotopy type theory and Voevodsky’s univalent foundations ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ Idempotents in intensional type theory ⋮ A univalent formalization of the p-adic numbers ⋮ Multisets in type theory ⋮ UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY

This page was built for publication: Voevodsky’s Univalence Axiom in Homotopy Type Theory