A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
From MaRDI portal
Publication:4635917
DOI10.1145/2933575.2934545zbMath1395.55011arXiv1605.03227OpenAlexW2963228298MaRDI QIDQ4635917
Kuen-Bang Hou (Favonia), Eric Finster, Peter LeFanu Lumsdaine, Daniel R. Licata
Publication date: 23 April 2018
Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1605.03227
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
Modalities in homotopy type theory ⋮ Internal languages of finitely complete \((\infty , 1)\)-categories ⋮ Strange new universes: Proof assistants and synthetic foundations ⋮ An introduction to univalent foundations for mathematicians ⋮ Unnamed Item ⋮ The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
This page was built for publication: A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
