{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/534","repository_url":"https://api.github.com/repos/UniMath/UniMath","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/534/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/534/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/534/events","html_url":"https://github.com/UniMath/UniMath/pull/534","id":198689119,"number":534,"title":"Added triangulated categories","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":110,"created_at":"2017-01-04T11:42:32Z","updated_at":"2017-02-24T16:26:59Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/UniMath/UniMath/pulls/534","html_url":"https://github.com/UniMath/UniMath/pull/534","diff_url":"https://github.com/UniMath/UniMath/pull/534.diff","patch_url":"https://github.com/UniMath/UniMath/pull/534.patch"},"body":"This pull request contains formalization of triangulated categories and a proof that K(A) has a\r\nstructure of a pretriangulated category. I try to add a proof that the octahedral axiom holds in\r\nK(A) later. Here is a summary of the changes.\r\n- Formalization of triangulated categories, HomologicalAlgebra/Triangulated.v\r\n  - PreTriang, pretriangulated category, line 688\r\n  - Triang, triangulated category, line 783\r\n  - TriangulatedFiveLemma, five lemma for triangulated categories, line 1556\r\n- I moved some code from Complexes.v to the following files\r\n  - KA.v, formalization of the naive homotopy category\r\n  - TranslationFunctors.v, translation functors for K(A) and C(A)\r\n  - MappingCone.v, formalization of mappping cones in C(A)\r\n  - MappingCylinder.v, formalization of mapping cylinders in C(A)\r\n- KATriangulated.v, formalization of the fact that K(A) has a structure of a pretriangulated \r\n  category, KAPreTriang, line 702.\r\n\r\nI did the following smaller change\r\n- I added iso_with_inv to precategories.v. This definition of isomorphism carries an inverse with\r\n  an isomorphism. The point of this is to have a computational inverse for an isomorphism. For\r\n  example, suppose f : X --> Y is an isomorphism of complexes. Then the morphism\r\n  `(inv_from_iso f) i`, i : hz, does not give a natural indexwise inverse Y i --> X i of\r\n  X i --> Y i. This became a problem when formalizing that K(A) is a pretriangulated category, where\r\n  I needed to use inverses of isomorphisms and prove commutativity of diagrams containing inverses."},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/282335405","html_url":"https://github.com/UniMath/UniMath/pull/534#issuecomment-282335405","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/534","id":282335405,"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},"created_at":"2017-02-24T16:26:59Z","updated_at":"2017-02-24T16:26:59Z","body":"@DanGrayson , this pull request is ready to be reconsidered.\r\nI wish to keep parameters in octahedral stuff visible."}}
{"actor":{"display_login":"tpannila"}}