Homotopies for Free!
Logic in Computer Science
2017-04-20 v2 Logic
Abstract
We show "free theorems" in the style of Wadler for polymorphic functions in homotopy type theory as consequences of the abstraction theorem. As an application, it follows that every space defined as a higher inductive type has the same homotopy groups as some type of polymorphic functions defined without univalence or higher inductive types.
Cite
@article{arxiv.1701.07937,
title = {Homotopies for Free!},
author = {Taichi Uemura},
journal= {arXiv preprint arXiv:1701.07937},
year = {2017}
}