Free Higher Groups in Homotopy Type Theory
Authors: Nicolai Kraus and Thorsten Altenkirch
Paper Information
| Title: | Free Higher Groups in Homotopy Type Theory |
| Authors: | Nicolai Kraus and Thorsten Altenkirch |
| Proceedings: | LICS PDF files |
| Editors: | Anuj Dawar and Erich Grädel |
| Keywords: | homotopy type theory, algebraic structures, truncation levels |
| Abstract: | ABSTRACT. Given a type A in homotopy type theory (HoTT), we define the free infinity-group on A as the higher inductive type FA with constructors [unit : FA], [cons : A -> FA -> FA], and conditions saying that every cons(a) is an auto-equivalence on FA. Assuming that A is a set (i.e. satisfies the principle of unique identity proofs), we are interested in the question whether FA is a set as well, which is very much related to an open problem in the HoTT book [Ex. 8.2]. In this paper, we show an approximation to the question, namely that the fundamental groups of FA are trivial. |
| Pages: | 10 |
| Talk: | Jul 09 11:40 (Session 47E) |
| Paper: | ![]() |
