The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory

DOI10.1145/2992783zbMath1367.03018arXiv1510.03918OpenAlexW2220627548MaRDI QIDQ5278189

Kristina Sojakova

Publication date: 13 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

torusunit circlehomotopy type theoryhigher inductive type

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40)

Related Items (1)

Cubical Agda: A dependently typed programming language with univalence and higher inductive types

Uses Software

• Coq
• GitHub

Cites Work

• π n (S n ) in Homotopy Type Theory
• Univalent Semantics of Constructive Type Theories
• A Cubical Approach to Synthetic Homotopy Theory
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory

This page was built for publication: The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory