{"action":"created","issue":{"url":"https://api.github.com/repos/HoTT/HoTT/issues/957","repository_url":"https://api.github.com/repos/HoTT/HoTT","labels_url":"https://api.github.com/repos/HoTT/HoTT/issues/957/labels{/name}","comments_url":"https://api.github.com/repos/HoTT/HoTT/issues/957/comments","events_url":"https://api.github.com/repos/HoTT/HoTT/issues/957/events","html_url":"https://github.com/HoTT/HoTT/issues/957","id":358224420,"node_id":"MDU6SXNzdWUzNTgyMjQ0MjA=","number":957,"title":"(c * (c * c)) doesn't unify with (c * c * c) for categories.","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":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":7,"created_at":"2018-09-07T22:01:09Z","updated_at":"2018-09-09T15:03:35Z","closed_at":null,"author_association":"NONE","body":"So we set up a coq file in HoTT like this:\r\n```\r\nRequire Import Categories.\r\n\r\nLocal Open Scope category_scope.\r\n\r\nContext {c : PreCategory}.\r\n```\r\nThen we run `Check (c*c*c).` and we get\r\n```\r\nc * c * c\r\n     : Core.PreCategory\r\n```\r\nNext we run `Check ((c*c)*c).` and we get\r\n```\r\nc * c * c\r\n     : Core.PreCategory\r\n```\r\nFinally we run `Check (c*(c*c)).` However this time we get\r\n```\r\nc * (c * c)\r\n     : Core.PreCategory\r\n```\r\nThis stops `c * c * c` and `c*(c*c)` from unifying.\r\nI presume this stems from assocativity not working for the product of categories.\r\n"},"comment":{"url":"https://api.github.com/repos/HoTT/HoTT/issues/comments/419721992","html_url":"https://github.com/HoTT/HoTT/issues/957#issuecomment-419721992","issue_url":"https://api.github.com/repos/HoTT/HoTT/issues/957","id":419721992,"node_id":"MDEyOklzc3VlQ29tbWVudDQxOTcyMTk5Mg==","user":{"login":"spitters","id":210638,"node_id":"MDQ6VXNlcjIxMDYzOA==","avatar_url":"https://avatars0.githubusercontent.com/u/210638?v=4","gravatar_id":"","url":"https://api.github.com/users/spitters","html_url":"https://github.com/spitters","followers_url":"https://api.github.com/users/spitters/followers","following_url":"https://api.github.com/users/spitters/following{/other_user}","gists_url":"https://api.github.com/users/spitters/gists{/gist_id}","starred_url":"https://api.github.com/users/spitters/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/spitters/subscriptions","organizations_url":"https://api.github.com/users/spitters/orgs","repos_url":"https://api.github.com/users/spitters/repos","events_url":"https://api.github.com/users/spitters/events{/privacy}","received_events_url":"https://api.github.com/users/spitters/received_events","type":"User","site_admin":false},"created_at":"2018-09-09T15:03:35Z","updated_at":"2018-09-09T15:03:35Z","author_association":"MEMBER","body":"There's a new generation of mathematicians being educated...\n\nOn Sun, Sep 9, 2018 at 3:58 PM Mike Shulman <notifications@github.com>\nwrote:\n\n> There are many things that it seems to the average mathematician that a\n> proof assistant \"should\" do automatically that proof assistants can't yet\n> do automatically. This is one of the reasons I think it will be a fairly\n> long time until all mathematics is formalized.\n>\n> —\n> You are receiving this because you commented.\n> Reply to this email directly, view it on GitHub\n> <https://github.com/HoTT/HoTT/issues/957#issuecomment-419717812>, or mute\n> the thread\n> <https://github.com/notifications/unsubscribe-auth/AAM2zhSGimzIQt2LRwcFK3LzS-ELYQw8ks5uZR6RgaJpZM4WfiOi>\n> .\n>\n"}}
{"actor":{"display_login":"spitters"}}