payload: {"action":"created","issue":{"url":"https://api.github.com/repos/HoTT/HoTT/issues/1139","repository_url":"https://api.github.com/repos/HoTT/HoTT","labels_url":"https://api.github.com/repos/HoTT/HoTT/issues/1139/labels{/name}","comments_url":"https://api.github.com/repos/HoTT/HoTT/issues/1139/comments","events_url":"https://api.github.com/repos/HoTT/HoTT/issues/1139/events","html_url":"https://github.com/HoTT/HoTT/issues/1139","id":527353854,"node_id":"MDU6SXNzdWU1MjczNTM4NTQ=","number":1139,"title":"Free groups","user":{"login":"Alizter","id":8614547,"node_id":"MDQ6VXNlcjg2MTQ1NDc=","avatar_url":"https://avatars1.githubusercontent.com/u/8614547?v=4","gravatar_id":"","url":"https://api.github.com/users/Alizter","html_url":"https://github.com/Alizter","followers_url":"https://api.github.com/users/Alizter/followers","following_url":"https://api.github.com/users/Alizter/following{/other_user}","gists_url":"https://api.github.com/users/Alizter/gists{/gist_id}","starred_url":"https://api.github.com/users/Alizter/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Alizter/subscriptions","organizations_url":"https://api.github.com/users/Alizter/orgs","repos_url":"https://api.github.com/users/Alizter/repos","events_url":"https://api.github.com/users/Alizter/events{/privacy}","received_events_url":"https://api.github.com/users/Alizter/received_events","type":"User","site_admin":false},"labels":[{"id":163418337,"node_id":"MDU6TGFiZWwxNjM0MTgzMzc=","url":"https://api.github.com/repos/HoTT/HoTT/labels/mathematics","name":"mathematics","color":"c7def8","default":false,"description":null}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":2,"created_at":"2019-11-22T18:40:35Z","updated_at":"2019-11-22T22:56:15Z","closed_at":null,"author_association":"COLLABORATOR","body":"I would like to construct the free group of a type A. I will probably need A to be a hset. The universal property of the free group F(-) will look something like this:\r\n\r\nGroupHom(F(A), G) <~> (A -> G)\r\n\r\nNow my plan for doing this is as follows:\r\n\r\n 1. Define the free group of a set A as F(A) := Pi 1 (Susp (A + 1)). \r\n 2. Start with a group homomorphism h : F(A) -> G\r\n 3. Promote this to the world of oo-groups using the classifying space construction: BF(A) -> BG, whereby it becomes a pointed map.\r\n 4. Observe that B ( Pi 1 X) <~> ||X||_1 which can be proven using the truncated Whitehead theorem from the HoTT book. Hence we have a pointed map: Susp (A + 1) -> BG.\r\n 5. Use the loop-susp adjunction to get a pointed map:  A + 1 -> loops BG, and observe that loops BG is pointed equivalent to G (pointed by identity element).\r\n 6. Observe that pointed maps A + 1 -> X are equivalent to maps A -> X. So we are done.\r\n\r\nSo we can get a recursion principal from this definition of free group for \"free\". The work that needs to be done is as follows:\r\n\r\n1. Prove the truncated Whitehead's theorem (The proof is in the book).\r\n2. Prove an isomorphism : Pi 1 X -> G implies a pointed equivalence X -> B G.\r\n3. Show that classifying spaces can turn groups into oo-groups.\r\n\r\nI am making a note of this argument here so I don't forget it in the future, as of now I have a formalization of classifying spaces but nothing about B (Pi 1 (X))."},"comment":{"url":"https://api.github.com/repos/HoTT/HoTT/issues/comments/557724627","html_url":"https://github.com/HoTT/HoTT/issues/1139#issuecomment-557724627","issue_url":"https://api.github.com/repos/HoTT/HoTT/issues/1139","id":557724627,"node_id":"MDEyOklzc3VlQ29tbWVudDU1NzcyNDYyNw==","user":{"login":"Alizter","id":8614547,"node_id":"MDQ6VXNlcjg2MTQ1NDc=","avatar_url":"https://avatars1.githubusercontent.com/u/8614547?v=4","gravatar_id":"","url":"https://api.github.com/users/Alizter","html_url":"https://github.com/Alizter","followers_url":"https://api.github.com/users/Alizter/followers","following_url":"https://api.github.com/users/Alizter/following{/other_user}","gists_url":"https://api.github.com/users/Alizter/gists{/gist_id}","starred_url":"https://api.github.com/users/Alizter/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Alizter/subscriptions","organizations_url":"https://api.github.com/users/Alizter/orgs","repos_url":"https://api.github.com/users/Alizter/repos","events_url":"https://api.github.com/users/Alizter/events{/privacy}","received_events_url":"https://api.github.com/users/Alizter/received_events","type":"User","site_admin":false},"created_at":"2019-11-22T22:56:15Z","updated_at":"2019-11-22T22:56:15Z","author_association":"COLLABORATOR","body":"Yes, Kraus and Altenkirch give another HIT construction which is kind of in between the two in the book. From experimenting with the James construction, recursive HITs can be very painful to work with, and the classical method of reduced words is very technical.\r\n\r\nIt seems that this way of constructing the free group might be simpler to define and work with than all three. I guess we will see :-)"}}
other: {"actor":{"display_login":"Alizter"}}