{"action":"created","issue":{"url":"https://api.github.com/repos/HoTT/HoTT/issues/654","labels_url":"https://api.github.com/repos/HoTT/HoTT/issues/654/labels{/name}","comments_url":"https://api.github.com/repos/HoTT/HoTT/issues/654/comments","events_url":"https://api.github.com/repos/HoTT/HoTT/issues/654/events","html_url":"https://github.com/HoTT/HoTT/issues/654","id":52947325,"number":654,"title":"Basic group theory","user":{"login":"mikeshulman","id":646600,"avatar_url":"https://avatars.githubusercontent.com/u/646600?v=3","gravatar_id":"","url":"https://api.github.com/users/mikeshulman","html_url":"https://github.com/mikeshulman","followers_url":"https://api.github.com/users/mikeshulman/followers","following_url":"https://api.github.com/users/mikeshulman/following{/other_user}","gists_url":"https://api.github.com/users/mikeshulman/gists{/gist_id}","starred_url":"https://api.github.com/users/mikeshulman/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mikeshulman/subscriptions","organizations_url":"https://api.github.com/users/mikeshulman/orgs","repos_url":"https://api.github.com/users/mikeshulman/repos","events_url":"https://api.github.com/users/mikeshulman/events{/privacy}","received_events_url":"https://api.github.com/users/mikeshulman/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":51,"created_at":"2014-12-27T03:52:59Z","updated_at":"2015-01-08T08:01:47Z","closed_at":null,"body":"For something I'm currently trying to formalize, I need some very basic group theory (specifically, [Lagrange's theorem](https://en.wikipedia.org/wiki/Lagrange%27s_theorem_%28group_theory%29)).  I could just prove the special case of it that I need, but as time goes on we'll undoubtedly need more group theory.  Is there any existing library including group theory (with a compatible license) that we could steal from?  Or is the HoTT approach to things like hsets, subsets, images, and quotients so different from any other that that wouldn't save any appreciable work?"},"comment":{"url":"https://api.github.com/repos/HoTT/HoTT/issues/comments/69147505","html_url":"https://github.com/HoTT/HoTT/issues/654#issuecomment-69147505","issue_url":"https://api.github.com/repos/HoTT/HoTT/issues/654","id":69147505,"user":{"login":"mikeshulman","id":646600,"avatar_url":"https://avatars.githubusercontent.com/u/646600?v=3","gravatar_id":"","url":"https://api.github.com/users/mikeshulman","html_url":"https://github.com/mikeshulman","followers_url":"https://api.github.com/users/mikeshulman/followers","following_url":"https://api.github.com/users/mikeshulman/following{/other_user}","gists_url":"https://api.github.com/users/mikeshulman/gists{/gist_id}","starred_url":"https://api.github.com/users/mikeshulman/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mikeshulman/subscriptions","organizations_url":"https://api.github.com/users/mikeshulman/orgs","repos_url":"https://api.github.com/users/mikeshulman/repos","events_url":"https://api.github.com/users/mikeshulman/events{/privacy}","received_events_url":"https://api.github.com/users/mikeshulman/received_events","type":"User","site_admin":false},"created_at":"2015-01-08T08:01:47Z","updated_at":"2015-01-08T08:01:47Z","body":"@andrejbauer I'd be surprised if you could get negation to be definitionally involutive, since the witness of decidability has to be carried around too, and symmetry on coproducts is not definitionally involutive.\r\n\r\n@aspiwack how do you define implication?  I would want `Holds (A -> B) = Holds A -> Holds B`; do you take `Denies (A -> B) = Holds A and Denies B`?\r\n"}}