{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/349","repository_url":"https://api.github.com/repos/UniMath/UniMath","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/349/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/349/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/349/events","html_url":"https://github.com/UniMath/UniMath/pull/349","id":149239263,"number":349,"title":"Filters and Topology","user":{"login":"cathlelay","id":9912958,"avatar_url":"https://avatars.githubusercontent.com/u/9912958?v=3","gravatar_id":"","url":"https://api.github.com/users/cathlelay","html_url":"https://github.com/cathlelay","followers_url":"https://api.github.com/users/cathlelay/followers","following_url":"https://api.github.com/users/cathlelay/following{/other_user}","gists_url":"https://api.github.com/users/cathlelay/gists{/gist_id}","starred_url":"https://api.github.com/users/cathlelay/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cathlelay/subscriptions","organizations_url":"https://api.github.com/users/cathlelay/orgs","repos_url":"https://api.github.com/users/cathlelay/repos","events_url":"https://api.github.com/users/cathlelay/events{/privacy}","received_events_url":"https://api.github.com/users/cathlelay/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2016-04-18T18:53:32Z","updated_at":"2016-04-18T19:59:54Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/UniMath/UniMath/pulls/349","html_url":"https://github.com/UniMath/UniMath/pull/349","diff_url":"https://github.com/UniMath/UniMath/pull/349.diff","patch_url":"https://github.com/UniMath/UniMath/pull/349.patch"},"body":"There is the first pull request about analysis.\r\nI formalize the notion of \"filter\" which is a generalization of neighborhoods and topological spaces.\r\nIt is based on the Bourbaki's book \"General Topology: Chapters 1-4\"."},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/211551416","html_url":"https://github.com/UniMath/UniMath/pull/349#issuecomment-211551416","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/349","id":211551416,"user":{"login":"andrejbauer","id":646599,"avatar_url":"https://avatars.githubusercontent.com/u/646599?v=3","gravatar_id":"","url":"https://api.github.com/users/andrejbauer","html_url":"https://github.com/andrejbauer","followers_url":"https://api.github.com/users/andrejbauer/followers","following_url":"https://api.github.com/users/andrejbauer/following{/other_user}","gists_url":"https://api.github.com/users/andrejbauer/gists{/gist_id}","starred_url":"https://api.github.com/users/andrejbauer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andrejbauer/subscriptions","organizations_url":"https://api.github.com/users/andrejbauer/orgs","repos_url":"https://api.github.com/users/andrejbauer/repos","events_url":"https://api.github.com/users/andrejbauer/events{/privacy}","received_events_url":"https://api.github.com/users/andrejbauer/received_events","type":"User","site_admin":false},"created_at":"2016-04-18T19:59:54Z","updated_at":"2016-04-18T19:59:54Z","body":"A small comment: you use `infinite_union` the general form of union that need not actually be infinite. It might be better to just call it `union` (or `general_union`, but I do not like that)."}}