Voevodsky’s Univalence Axiom in Homotopy Type Theory
From MaRDI portal
Publication:3193040
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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