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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 2015
Accession Number
AD1003367

Entities

People

  • Kristina Sojakova

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Air Force
  • Algebraic Topology
  • Computations
  • Computer Science
  • Elimination
  • Geometry
  • Identities
  • Inductors
  • Mathematics
  • Scientific Research
  • Topology
  • Transport Ships

Fields of Study

  • Mathematics

Readers

  • Mathematical Modeling and Probability Theory.
  • Wave Propagation and Nonlinear Chaotic Dynamics.