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: |