Free higher groups in homotopy type theory

Nicolai Kraus, Thorsten Altenkirch

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)
96 Downloads (Pure)

Abstract

Given a type A in homotopy type theory (HoTT), we can define the free ∞-group on A as the loop space of the suspension of A + 1. Equivalently, this free higher group can be defined as a higher inductive type F(A) with constructors unit: F(A), cons: A→F(A)→F(A), and conditions saying that every cons(a) is an auto-equivalence on F(A). Assuming that A is a set (i.e. satisfies the principle of unique identity proofs), we are interested in the question whether F(A) is a set as well, which is very much related to an open problem in the HoTT book [22, Ex. 8.2]. We show an approximation to the question, namely that the fundamental groups of F(A) are trivial, i.e. that ||F(A)||1 is a set.
Original languageEnglish
Title of host publicationThirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018)
PublisherAssociation for Computing Machinery (ACM)
Pages599-608
ISBN (Electronic)9781450355834
DOIs
Publication statusPublished - 9 Jul 2018
EventThirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018) - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018

Conference

ConferenceThirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018)
Country/TerritoryUnited Kingdom
CityOxford
Period9/07/1812/07/18

Fingerprint

Dive into the research topics of 'Free higher groups in homotopy type theory'. Together they form a unique fingerprint.

Cite this