| ||||
| ||||
![]() Title:Free Higher Groups in Homotopy Type Theory Conference:LICS18 Tags:algebraic structures, homotopy type theory and truncation levels 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. | ||||
Copyright © 2002 – 2025 EasyChair |