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

Categorical logic, topoi (03G30) Mechanization of proofs and logical operations (03B35) Topological categories, foundations of homotopy theory (55U40)

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