Free higher groups in homotopy type theory
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...
| Main Authors: | , |
|---|---|
| Format: | Conference or Workshop Item |
| Language: | English |
| Published: |
2018
|
| Online Access: | https://eprints.nottingham.ac.uk/51212/ |
| _version_ | 1848798443844141056 |
|---|---|
| author | Kraus, Nicolai Altenkirch, Thorsten |
| author_facet | Kraus, Nicolai Altenkirch, Thorsten |
| author_sort | Kraus, Nicolai |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T20:19:52Z |
| format | Conference or Workshop Item |
| id | nottingham-51212 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T20:19:52Z |
| publishDate | 2018 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-512122018-09-20T10:13:16Z https://eprints.nottingham.ac.uk/51212/ Free higher groups in homotopy type theory Kraus, Nicolai Altenkirch, Thorsten 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. 2018-07-09 Conference or Workshop Item PeerReviewed application/pdf en https://eprints.nottingham.ac.uk/51212/1/root_lics_fg.pdf Kraus, Nicolai and Altenkirch, Thorsten (2018) Free higher groups in homotopy type theory. In: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 9–12 July 2018, Oxford, England. https://dl.acm.org/citation.cfm?id=3209183 |
| spellingShingle | Kraus, Nicolai Altenkirch, Thorsten Free higher groups in homotopy type theory |
| title | Free higher groups in homotopy type theory |
| title_full | Free higher groups in homotopy type theory |
| title_fullStr | Free higher groups in homotopy type theory |
| title_full_unstemmed | Free higher groups in homotopy type theory |
| title_short | Free higher groups in homotopy type theory |
| title_sort | free higher groups in homotopy type theory |
| url | https://eprints.nottingham.ac.uk/51212/ https://eprints.nottingham.ac.uk/51212/ |