{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/mathlib/issues/390","repository_url":"https://api.github.com/repos/leanprover/mathlib","labels_url":"https://api.github.com/repos/leanprover/mathlib/issues/390/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/mathlib/issues/390/comments","events_url":"https://api.github.com/repos/leanprover/mathlib/issues/390/events","html_url":"https://github.com/leanprover/mathlib/pull/390","id":367116490,"node_id":"MDExOlB1bGxSZXF1ZXN0MjIwNjI3OTg2","number":390,"title":"Extract bundled from category_theory and generalize to Sort","user":{"login":"spl","id":54900,"node_id":"MDQ6VXNlcjU0OTAw","avatar_url":"https://avatars0.githubusercontent.com/u/54900?v=4","gravatar_id":"","url":"https://api.github.com/users/spl","html_url":"https://github.com/spl","followers_url":"https://api.github.com/users/spl/followers","following_url":"https://api.github.com/users/spl/following{/other_user}","gists_url":"https://api.github.com/users/spl/gists{/gist_id}","starred_url":"https://api.github.com/users/spl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/spl/subscriptions","organizations_url":"https://api.github.com/users/spl/orgs","repos_url":"https://api.github.com/users/spl/repos","events_url":"https://api.github.com/users/spl/events{/privacy}","received_events_url":"https://api.github.com/users/spl/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":2,"created_at":"2018-10-05T08:48:44Z","updated_at":"2018-10-07T00:04:46Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/leanprover/mathlib/pulls/390","html_url":"https://github.com/leanprover/mathlib/pull/390","diff_url":"https://github.com/leanprover/mathlib/pull/390.diff","patch_url":"https://github.com/leanprover/mathlib/pull/390.patch"},"body":"* Extracted `bundled` from `category_theory.category`\r\n* Extracted `bundled.map` from `category_theory.functor`\r\n* Renamed `str` to `inst`\r\n* Added bundled `decidable_eq`.\r\n\r\nSee this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/bundled.20in.20category_theory/near/135174961)."},"comment":{"url":"https://api.github.com/repos/leanprover/mathlib/issues/comments/427615086","html_url":"https://github.com/leanprover/mathlib/pull/390#issuecomment-427615086","issue_url":"https://api.github.com/repos/leanprover/mathlib/issues/390","id":427615086,"node_id":"MDEyOklzc3VlQ29tbWVudDQyNzYxNTA4Ng==","user":{"login":"semorrison","id":477956,"node_id":"MDQ6VXNlcjQ3Nzk1Ng==","avatar_url":"https://avatars1.githubusercontent.com/u/477956?v=4","gravatar_id":"","url":"https://api.github.com/users/semorrison","html_url":"https://github.com/semorrison","followers_url":"https://api.github.com/users/semorrison/followers","following_url":"https://api.github.com/users/semorrison/following{/other_user}","gists_url":"https://api.github.com/users/semorrison/gists{/gist_id}","starred_url":"https://api.github.com/users/semorrison/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/semorrison/subscriptions","organizations_url":"https://api.github.com/users/semorrison/orgs","repos_url":"https://api.github.com/users/semorrison/repos","events_url":"https://api.github.com/users/semorrison/events{/privacy}","received_events_url":"https://api.github.com/users/semorrison/received_events","type":"User","site_admin":false},"created_at":"2018-10-07T00:04:46Z","updated_at":"2018-10-07T00:04:46Z","author_association":"CONTRIBUTOR","body":"> @semorrison You complained that this wasn't as useful as you hoped, because you quickly needed to bundle more than 1 thing. We have `lift_on_2` etc... Would it make sense to also have `bundled_2` and `bundled_3`?\r\n\r\nNo, I don't think so. It's already a pity that using `bundled` means we don't get a custom name; once it's a more complicated object, I think it's worth the boilerplate in order to achieve a short name. `CpltTopRing` is a much better name than `bundled_3 ring topological_ring complete` or whatever it would be."}}
{"actor":{"display_login":"semorrison"}}