DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
Accession Number:
AD1003367
Title:
The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory
Corporate Author:
Carnegie Mellon University Pittsburgh United States
Report Date:
2015-09-01
Abstract:
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.
Descriptive Note:
Technical Report
Pages:
0023
Distribution Statement:
Approved For Public Release;
File Size:
0.37MB
