Skip to main content

Research Repository

See what's under the surface

Advanced Search

Free higher groups in homotopy type theory

Kraus, Nicolai; Altenkirch, Thorsten

Authors

Nicolai Kraus nicolai.kraus@nottingham.ac.uk

Thorsten Altenkirch txa@cs.nott.ac.uk



Abstract

Given a type A in homotopy type theory (HoTT), we can define the free ∞-group on A as the 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). Equivalently, we can take the loop space of the suspension of A + 1. 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 [20, 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.

Start Date Jul 9, 2018
Publication Date Jul 12, 2018
Electronic ISSN 1043-6871
Publisher Association for Computing Machinery (ACM)
Peer Reviewed Peer Reviewed
Pages 599-608
Book Title LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
ISBN 978-1-4503-5583-4
APA6 Citation Kraus, N., & Altenkirch, T. (2018). Free higher groups in homotopy type theory. In LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 599-608. doi:10.1145/3209108.3209183
DOI https://doi.org/10.1145/3209108.3209183
Publisher URL https://dl.acm.org/citation.cfm?id=3209183
Related Public URLs https://lics.siglog.org/lics18/
Copyright Statement Copyright information regarding this work can be found at the following address: http://eprints.nottingh.../end_user_agreement.pdf
Additional Information

Composition Type:

Files

root_lics_fg.pdf (756 Kb)
PDF

Copyright Statement
Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf





You might also like



Downloadable Citations

;