CMU-CS-15-105Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-15-105
Kristina Sojakova September 2015
Keywords:
Homotopy type theory, torus, unit circle, higher inductive type
Homotopy type theory is a new branch of mathematics which merges insights from abstract homotopy theory and higher category theory with those of logic and type theory. It allows us to represent a variety of mathematical objects as basic type-theoretic constructions, higher inductive types. We present a proof that in homotopy type theory, the torus is equivalent to the product of two circles. This result indicates that the synthetic definition of torus as a higher inductive type is indeed correct. 23 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |