{"action":"opened","issue":{"url":"https://api.github.com/repos/HoTT/book/issues/920","repository_url":"https://api.github.com/repos/HoTT/book","labels_url":"https://api.github.com/repos/HoTT/book/issues/920/labels{/name}","comments_url":"https://api.github.com/repos/HoTT/book/issues/920/comments","events_url":"https://api.github.com/repos/HoTT/book/issues/920/events","html_url":"https://github.com/HoTT/book/issues/920","id":176192640,"number":920,"title":"Suggestion of an exercise about connectedness","user":{"login":"koba-e964","id":3303362,"avatar_url":"https://avatars.githubusercontent.com/u/3303362?v=3","gravatar_id":"","url":"https://api.github.com/users/koba-e964","html_url":"https://github.com/koba-e964","followers_url":"https://api.github.com/users/koba-e964/followers","following_url":"https://api.github.com/users/koba-e964/following{/other_user}","gists_url":"https://api.github.com/users/koba-e964/gists{/gist_id}","starred_url":"https://api.github.com/users/koba-e964/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/koba-e964/subscriptions","organizations_url":"https://api.github.com/users/koba-e964/orgs","repos_url":"https://api.github.com/users/koba-e964/repos","events_url":"https://api.github.com/users/koba-e964/events{/privacy}","received_events_url":"https://api.github.com/users/koba-e964/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2016-09-10T17:55:50Z","updated_at":"2016-09-10T17:55:50Z","closed_at":null,"body":"How about adding an exercise about connectedness like:\r\nAssuming LEM, show that types are connected if and only if they are categorically connected, i.e. for every $A: \\type$ we have\r\n```\r\n\\iscontr(\\trunc 0{A}) \\eqvsym ((\\prd{B,C: \\type} (A \\to B) + (A \\to C) \\eqvsym (A \\to B + C)).\r\n```\r\n? (The definition of categorical connectedness is from [nLab](https://ncatlab.org/nlab/show/connected+space).)\r\n\r\nI believe I obtained this result assuming LEM, but I don't know whether LEM is necessary or not. In addition, I think propositional resizing is necessary to avoid universe problems (the right-hand side is in the next higher universe than A, B and C). \r\n\r\nIf we add this, I think it is appropriate to add it to Chapter 7's Exercises.\r\n"}}
{"actor":{"display_login":"koba-e964"}}