FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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: