{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/414","repository_url":"https://api.github.com/repos/UniMath/UniMath","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/414/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/414/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/414/events","html_url":"https://github.com/UniMath/UniMath/pull/414","id":168455944,"number":414,"title":"Added short exact sequences","user":{"login":"tpannila","id":3755739,"avatar_url":"https://avatars.githubusercontent.com/u/3755739?v=3","gravatar_id":"","url":"https://api.github.com/users/tpannila","html_url":"https://github.com/tpannila","followers_url":"https://api.github.com/users/tpannila/followers","following_url":"https://api.github.com/users/tpannila/following{/other_user}","gists_url":"https://api.github.com/users/tpannila/gists{/gist_id}","starred_url":"https://api.github.com/users/tpannila/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/tpannila/subscriptions","organizations_url":"https://api.github.com/users/tpannila/orgs","repos_url":"https://api.github.com/users/tpannila/repos","events_url":"https://api.github.com/users/tpannila/events{/privacy}","received_events_url":"https://api.github.com/users/tpannila/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":22,"created_at":"2016-07-30T08:01:47Z","updated_at":"2016-09-09T19:30:09Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/UniMath/UniMath/pulls/414","html_url":"https://github.com/UniMath/UniMath/pull/414","diff_url":"https://github.com/UniMath/UniMath/pull/414.diff","patch_url":"https://github.com/UniMath/UniMath/pull/414.patch"},"body":"This pull request contains formalization of short exact sequences. There are\r\n4 definitions:\r\n- ShortShortExact for  A -> B -> C.\r\n- LeftShortExact and RightShortExact for 0 -> A -> B -> C and A -> B -> C -> 0,\r\n  respectively.\r\n- ShortExact for 0 -> A -> B -> C -> 0\r\n\r\nUsing factorization property for morphisms of Abelian_precategory, the\r\nfollowing are formalized:\r\n- Construct the canonical ShortExact from ShortShortExact by using image and\r\n  coimage.\r\n- A criteria for constructing ShortShortExact from data similar to the\r\n  canonical ShortExact obtained from ShortShortExact.\r\n\r\nAll comments are welcome.\r\n"},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/246015254","html_url":"https://github.com/UniMath/UniMath/pull/414#issuecomment-246015254","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/414","id":246015254,"user":{"login":"DanGrayson","id":700228,"avatar_url":"https://avatars.githubusercontent.com/u/700228?v=3","gravatar_id":"","url":"https://api.github.com/users/DanGrayson","html_url":"https://github.com/DanGrayson","followers_url":"https://api.github.com/users/DanGrayson/followers","following_url":"https://api.github.com/users/DanGrayson/following{/other_user}","gists_url":"https://api.github.com/users/DanGrayson/gists{/gist_id}","starred_url":"https://api.github.com/users/DanGrayson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DanGrayson/subscriptions","organizations_url":"https://api.github.com/users/DanGrayson/orgs","repos_url":"https://api.github.com/users/DanGrayson/repos","events_url":"https://api.github.com/users/DanGrayson/events{/privacy}","received_events_url":"https://api.github.com/users/DanGrayson/received_events","type":"User","site_admin":false},"created_at":"2016-09-09T19:30:09Z","updated_at":"2016-09-09T19:30:09Z","body":"Re \"Cannot chage Abelian_AbelianData1 to AbelianData1 because it exists already in Abelian.v. Similarly for AbelianData2. This should not be a big problem because one almost never uses these definitions directly. One uses Zero, BinProducts, BinCoproducts, Kernels, and Cokernels.\"\r\n\r\nI have in mind people reading your files, not the ultimate users\r\n\r\nThere are many identifiers in Abelian.v that have Abelian as a prefix.  Such prefixes are not needed to distinguish these things from each other.  For example, `AbelianData1` could be `Data1`.\r\n\r\nThe type of `Abelian_AbelianData1` is `AbelianPreCat -> AbelianData1 A`.   It might be good to try to find names for functions that give at hint at them being functions and at what they do.  \r\n\r\nIn addition, all these functions should have analogous names:\r\n```\r\n  (** Accessor functions Abelian. *)\r\n  Definition Zero : Zero A := pr1 (pr2 (pr1 A)).\r\n  Definition BinProducts : BinProducts A := pr1 (pr2 (pr2 (pr1 A))).\r\n  Definition BinCoproducts : BinCoproducts A := pr2 (pr2 (pr2 (pr1 A))).\r\n  Definition Abelian_AbelianData1 : AbelianData1 A := (pr2 (pr1 A)).\r\n  Definition Kernels : Kernels Zero := pr1 (pr1 (pr2 A)).\r\n  Definition Cokernels : Cokernels Zero := pr2 (pr1 (pr2 A)).\r\n  Definition Abelian_AbelianData2 : AbelianData2 A Abelian_AbelianData1 := pr1 (pr2 A).\r\n  Definition AMKD : AbelianMonicKernelsData A (pr2 (pr1 A)) := pr1 (pr2 (pr2 A)).\r\n  Definition AECD : AbelianEpiCokernelsData A (pr2 (pr1 A)) := pr2 (pr2 (pr2 A)).\r\n```\r\nThe line `Definition BinProducts : BinProducts A := pr1 (pr2 (pr2 (pr1 A))).` is confusing because the two `BinProducts`s are different sorts of things: one is a type and the other is not.\r\n \r\nPerhaps one could implement a way to distinguish accessor functions from other things, so they fit together and don't tend to get read as types.  For example, they could all start with \"to\".  Then we could have this:\r\n```\r\n  (** Accessor functions Abelian. *)\r\n  Definition toZero : Zero A := pr1 (pr2 (pr1 A)).\r\n  Definition toBinProducts : BinProducts A := pr1 (pr2 (pr2 (pr1 A))).\r\n  Definition toBinCoproducts : BinCoproducts A := pr2 (pr2 (pr2 (pr1 A))).\r\n  Definition toData1 : Data1 A := (pr2 (pr1 A)).\r\n  Definition toKernels : Kernels Zero := pr1 (pr1 (pr2 A)).\r\n  Definition toCokernels : Cokernels Zero := pr2 (pr1 (pr2 A)).\r\n  Definition toData2 : Data2 A Abelian_AbelianData1 := pr1 (pr2 A).\r\n  Definition toAMKD : AbelianMonicKernelsData A (pr2 (pr1 A)) := pr1 (pr2 (pr2 A)).\r\n  Definition toAECD : AbelianEpiCokernelsData A (pr2 (pr1 A)) := pr2 (pr2 (pr2 A)).\r\n```\r\nThere might be other good ideas.\r\n"}}
{"actor":{"display_login":"DanGrayson"}}