π n (S n ) in Homotopy Type Theory
From MaRDI portal
Publication:2938036
DOI10.1007/978-3-319-03545-1_1zbMath1427.03033OpenAlexW84482504MaRDI QIDQ2938036
Daniel R. Licata, Guillaume Brunerie
Publication date: 13 January 2015
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-03545-1_1
Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40) Type theory (03B38)
Related Items (5)
The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory ⋮ Adjoint Logic with a 2-Category of Modes ⋮ Unnamed Item ⋮ Formalization of the fundamental group in untyped set theory using auto2 ⋮ Unnamed Item
This page was built for publication: π n (S n ) in Homotopy Type Theory
