Free higher groups in homotopy type theory

Nicolai Kraus; Thorsten Altenkirch

doi:10.1145/3209108.3209183

Free higher groups in homotopy type theory

Nicolai Kraus, Thorsten Altenkirch

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

4 Citations (Scopus)

151 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)||₁ is a set.

Original language	English
Title of host publication	Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018)
Publisher	Association for Computing Machinery (ACM)
Pages	599-608
ISBN (Electronic)	9781450355834
DOIs	https://doi.org/10.1145/3209108.3209183
Publication status	Published - 9 Jul 2018
Event	Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018) - Oxford, United Kingdom Duration: 9 Jul 2018 → 12 Jul 2018

Conference

Conference	Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018)
Country/Territory	United Kingdom
City	Oxford
Period	9/07/18 → 12/07/18

Access to Document

10.1145/3209108.3209183Licence: None: All rights reserved

Kraus_&_Altenkirch_Free_higher_groups_in_homotopy_type_theory_LICS_2018Accepted author manuscript, 755 KBLicence: None: All rights reserved

http://dl.acm.org/citation.cfm?doid=3209108.3209183Licence: None: All rights reserved

Cite this

@inproceedings{dc2ba16c10fd4c188a6afc65339e416d,

title = "Free higher groups in homotopy type theory",

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.",

author = "Nicolai Kraus and Thorsten Altenkirch",

year = "2018",

month = jul,

day = "9",

doi = "10.1145/3209108.3209183",

language = "English",

pages = "599--608",

booktitle = "Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018)",

publisher = "Association for Computing Machinery (ACM)",

address = "United States",

note = "Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018) ; Conference date: 09-07-2018 Through 12-07-2018",

}

TY - GEN

T1 - Free higher groups in homotopy type theory

AU - Kraus, Nicolai

AU - Altenkirch, Thorsten

PY - 2018/7/9

Y1 - 2018/7/9

N2 - 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.

AB - 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.

U2 - 10.1145/3209108.3209183

DO - 10.1145/3209108.3209183

M3 - Conference contribution

SP - 599

EP - 608

BT - Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018)

PB - Association for Computing Machinery (ACM)

T2 - Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018)

Y2 - 9 July 2018 through 12 July 2018

ER -

Free higher groups in homotopy type theory

Abstract

Conference

Access to Document

Fingerprint

Cite this