{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/409","repository_url":"https://api.github.com/repos/UniMath/UniMath","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/409/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/409/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/409/events","html_url":"https://github.com/UniMath/UniMath/pull/409","id":166701727,"number":409,"title":"Bicategories Definitions","user":{"login":"mvr","id":10843,"avatar_url":"https://avatars.githubusercontent.com/u/10843?v=3","gravatar_id":"","url":"https://api.github.com/users/mvr","html_url":"https://github.com/mvr","followers_url":"https://api.github.com/users/mvr/followers","following_url":"https://api.github.com/users/mvr/following{/other_user}","gists_url":"https://api.github.com/users/mvr/gists{/gist_id}","starred_url":"https://api.github.com/users/mvr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mvr/subscriptions","organizations_url":"https://api.github.com/users/mvr/orgs","repos_url":"https://api.github.com/users/mvr/repos","events_url":"https://api.github.com/users/mvr/events{/privacy}","received_events_url":"https://api.github.com/users/mvr/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":27,"created_at":"2016-07-20T22:57:37Z","updated_at":"2016-09-27T15:08:46Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/UniMath/UniMath/pulls/409","html_url":"https://github.com/UniMath/UniMath/pull/409","diff_url":"https://github.com/UniMath/UniMath/pull/409.diff","patch_url":"https://github.com/UniMath/UniMath/pull/409.patch"},"body":"We define prebicategories, internal equivalences and bicategories. We prove that Cat and PreCat are prebicategories (but not that Cat is a bicategory).\r\n\r\nThere is also some initial work on showing that paths between precategories are equivalent to isomorphisms of precategories, as defined in the univalent categories paper. There are maps (A = B) <-> (catiso A B), but proving that they are inverse turned out to be beyond me."},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/249893593","html_url":"https://github.com/UniMath/UniMath/pull/409#issuecomment-249893593","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/409","id":249893593,"user":{"login":"vladimirias","id":424011,"avatar_url":"https://avatars.githubusercontent.com/u/424011?v=3","gravatar_id":"","url":"https://api.github.com/users/vladimirias","html_url":"https://github.com/vladimirias","followers_url":"https://api.github.com/users/vladimirias/followers","following_url":"https://api.github.com/users/vladimirias/following{/other_user}","gists_url":"https://api.github.com/users/vladimirias/gists{/gist_id}","starred_url":"https://api.github.com/users/vladimirias/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/vladimirias/subscriptions","organizations_url":"https://api.github.com/users/vladimirias/orgs","repos_url":"https://api.github.com/users/vladimirias/repos","events_url":"https://api.github.com/users/vladimirias/events{/privacy}","received_events_url":"https://api.github.com/users/vladimirias/received_events","type":"User","site_admin":false},"created_at":"2016-09-27T15:08:45Z","updated_at":"2016-09-27T15:08:45Z","body":"What I do not understand is where the precategory_binproduct is from. It does not show up in the definition of pre-bicategory, does it?\n\n> On Sep 27, 2016, at 10:14 AM, Mitchell Riley <notifications@github.com> wrote:\n> \n> We need to define a natural transformation between F (G H) and (F G) H, this \"Step 1\", and the natural transformation is of course (fun a => identity _). But we also need to show that this natural transformation is itself natural in F, G and H, this is \"Step 2\".\n> \n> The proof of the pentagon is further down the file in Catlike_pentagon, and it's indeed almost reflexivity, although we have to cancel some identity morphisms.\n> \n> —\n> You are receiving this because you commented.\n> Reply to this email directly, view it on GitHub <https://github.com/UniMath/UniMath/pull/409#issuecomment-249877395>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAZ4S-s1hT6S3ygoZUu4_Az3isIPISYTks5quSSvgaJpZM4JRSoC>.\n> \n\n"}}
{"actor":{"display_login":"vladimirias"}}