Calculating the Fundamental Group of the Circle in Homotopy Type Theory

DOI10.1109/LICS.2013.28zbMath1369.03097arXiv1301.3443OpenAlexW2062764235MaRDI QIDQ5271059

Michael Shulman, Daniel R. Licata

Publication date: 3 July 2017

Published in: 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Related Items (15)

The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory ⋮ Adjoint Logic with a 2-Category of Modes ⋮ The construction of set-truncated higher inductive types ⋮ Homotopical patch theory ⋮ Unnamed Item ⋮ Naïve Type Theory ⋮ The Hurewicz theorem in homotopy type theory ⋮ Strange new universes: Proof assistants and synthetic foundations ⋮ Eliminating dependent pattern matching without K ⋮ Type-theoretic approaches to ordinals ⋮ Unnamed Item ⋮ Mathesis Universalis and Homotopy Type Theory ⋮ Brouwer's fixed-point theorem in real-cohesive homotopy type theory ⋮ An introduction to univalent foundations for mathematicians ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types

This page was built for publication: Calculating the Fundamental Group of the Circle in Homotopy Type Theory