{"action":"created","comment":{"url":"https://api.github.com/repos/HoTT/book/pulls/comments/81442485","pull_request_review_id":2425206,"id":81442485,"diff_hunk":"@@ -1467,6 +1467,62 @@ \\subsection*{Solution to \\cref{ex:is-conn-trunc-functor}}\n   &= (t \\circ \\tprojf k)(a) \\tag{since $g$ is a section of $\\lam{s} s\\circ f$}\\\\\n   & \\equiv t(\\tproj ka).\n \\end{align*}\n+\\subsection*{Solution to \\cref{ex:categorical-connectivity}}\n+\n+Let us denote by $\\mathsf{isConn}(A)$ the connectivity of type $A$. It is known that\n+\\begin{displaymath}\n+ \\mathsf{isConn}(A) \\simeq \\trunc {} A \\times \\prd{x,y:A} \\trunc {} {\\id[A]xy}\n+\\end{displaymath}\n+(see \\cref{ex:connectivity-inductively}).\n+\\begin{enumerate}\n+ \\item Suppose a type $A$ is connected. The goal $\\prd{B,C:\\type} \\isequiv(e_{A,B,C})$ is a mere proposition, so we can assume $a:A$ and $\\prd{x,y:A} \\trunc {} {x = y}$.\n+\n+       Let $B,C$ be types. We want to construct $h:(A\\to B+C) \\to (A\\to B)+(A\\to C)$ such that $h \\circ e = \\idfunc$ and $e \\circ h = \\idfunc$.\n+       Let $f:A \\to B+C$ be an arbitrary function. We have case analysis on $f(a):B + C$.\\\\\n+       (a) if $f(a) \\equiv \\inl(u)$ for some $u:B$:\n+       We want a function $g:A\\to B$ such that $f(x) = \\inl(g(x))$ for every $x:A$. Let us define $k:B+C\\to B$ by\n+       \\begin{align*}\n+\tk(\\inl(b)) &\\defeq b;\\\\\n+\tk(\\inr(c)) &\\defeq f(a) \\enspace,\n+       \\end{align*}\n+       and $g \\defeq k \\circ f$. Then we have $\\inl(g(x)) = \\inl(k(f(x))) = f(x)$ for every $x:A$ (by case analysis on $f(x)$ and $\\trunc {} {\\id[A]{a}{x}}$).\n+       With this $g$, we define $h(f) \\defeq \\inl(g)$. Then we have\n+       \\begin{displaymath}\n+\te_{A,B,C}(h(f)) = e_{A,B,C}(\\inl(g)) = \\lam{x} \\inl(g(x)) = f\n+       \\end{displaymath}\n+       and\n+       \\begin{displaymath}\n+\th(e_{A,B,C}(\\inl(v))) = h(\\lam{x} \\inl(v(x))) = \\lam{x} k(\\inl(v(x))) = v\n+       \\end{displaymath}\n+       for any $v: A\\to B$.\\\\\n+       (b) if $f(a) \\equiv \\inr(u)$ for some $u:C$: Similar to (a).\\\\\n+ \\item (Categorial connectivity to $\\mathsf{isConn}$ implies $\\LEM{}$):\n+       Assume for every type $A$,\n+       $(\\prd{B,C:\\type}\\isequiv(e_{A,B,C})) \\to \\mathsf{isConn}(A)$.","path":"exercise_solutions.tex","position":null,"original_position":35,"commit_id":"c89b3a90e60a83d134aa5545bd42b14046c2e73e","original_commit_id":"c668af7223d6533b15ea4f4ea638f9f4013cf787","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},"body":"Fixed in c89b3a9.","created_at":"2016-10-01T03:08:25Z","updated_at":"2016-10-01T03:08:25Z","html_url":"https://github.com/HoTT/book/pull/921#discussion_r81442485","pull_request_url":"https://api.github.com/repos/HoTT/book/pulls/921","_links":{"self":{"href":"https://api.github.com/repos/HoTT/book/pulls/comments/81442485"},"html":{"href":"https://github.com/HoTT/book/pull/921#discussion_r81442485"},"pull_request":{"href":"https://api.github.com/repos/HoTT/book/pulls/921"}}},"pull_request":{"url":"https://api.github.com/repos/HoTT/book/pulls/921","id":85346587,"html_url":"https://github.com/HoTT/book/pull/921","diff_url":"https://github.com/HoTT/book/pull/921.diff","patch_url":"https://github.com/HoTT/book/pull/921.patch","issue_url":"https://api.github.com/repos/HoTT/book/issues/921","number":921,"state":"open","locked":false,"title":"Add Exercise (categorical connectivity, #920)","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},"body":"Fix #920.\r\nThis exercise will be appended to the last of Exercise 7, so it will change no numbering.\r\n\r\nHere are some questions:\r\n(1) Is the solution to this exercise needed? If so, I think I can write it.\r\n(2) Is an errata needed?\r\n(3) Is the index `\\makeindex{connected!categorically}` sufficient, or do we need extra `\\makeindex`s?","created_at":"2016-09-15T05:17:44Z","updated_at":"2016-10-01T03:08:25Z","closed_at":null,"merged_at":null,"merge_commit_sha":"4ac186eec5367977e7a714c8d0feb5c683c7773e","assignee":null,"assignees":[],"milestone":null,"commits_url":"https://api.github.com/repos/HoTT/book/pulls/921/commits","review_comments_url":"https://api.github.com/repos/HoTT/book/pulls/921/comments","review_comment_url":"https://api.github.com/repos/HoTT/book/pulls/comments{/number}","comments_url":"https://api.github.com/repos/HoTT/book/issues/921/comments","statuses_url":"https://api.github.com/repos/HoTT/book/statuses/c89b3a90e60a83d134aa5545bd42b14046c2e73e","head":{"label":"koba-e964:ex-7","ref":"ex-7","sha":"c89b3a90e60a83d134aa5545bd42b14046c2e73e","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},"repo":{"id":65350565,"name":"book","full_name":"koba-e964/book","owner":{"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},"private":false,"html_url":"https://github.com/koba-e964/book","description":"A textbook on informal homotopy type theory","fork":true,"url":"https://api.github.com/repos/koba-e964/book","forks_url":"https://api.github.com/repos/koba-e964/book/forks","keys_url":"https://api.github.com/repos/koba-e964/book/keys{/key_id}","collaborators_url":"https://api.github.com/repos/koba-e964/book/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/koba-e964/book/teams","hooks_url":"https://api.github.com/repos/koba-e964/book/hooks","issue_events_url":"https://api.github.com/repos/koba-e964/book/issues/events{/number}","events_url":"https://api.github.com/repos/koba-e964/book/events","assignees_url":"https://api.github.com/repos/koba-e964/book/assignees{/user}","branches_url":"https://api.github.com/repos/koba-e964/book/branches{/branch}","tags_url":"https://api.github.com/repos/koba-e964/book/tags","blobs_url":"https://api.github.com/repos/koba-e964/book/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/koba-e964/book/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/koba-e964/book/git/refs{/sha}","trees_url":"https://api.github.com/repos/koba-e964/book/git/trees{/sha}","statuses_url":"https://api.github.com/repos/koba-e964/book/statuses/{sha}","languages_url":"https://api.github.com/repos/koba-e964/book/languages","stargazers_url":"https://api.github.com/repos/koba-e964/book/stargazers","contributors_url":"https://api.github.com/repos/koba-e964/book/contributors","subscribers_url":"https://api.github.com/repos/koba-e964/book/subscribers","subscription_url":"https://api.github.com/repos/koba-e964/book/subscription","commits_url":"https://api.github.com/repos/koba-e964/book/commits{/sha}","git_commits_url":"https://api.github.com/repos/koba-e964/book/git/commits{/sha}","comments_url":"https://api.github.com/repos/koba-e964/book/comments{/number}","issue_comment_url":"https://api.github.com/repos/koba-e964/book/issues/comments{/number}","contents_url":"https://api.github.com/repos/koba-e964/book/contents/{+path}","compare_url":"https://api.github.com/repos/koba-e964/book/compare/{base}...{head}","merges_url":"https://api.github.com/repos/koba-e964/book/merges","archive_url":"https://api.github.com/repos/koba-e964/book/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/koba-e964/book/downloads","issues_url":"https://api.github.com/repos/koba-e964/book/issues{/number}","pulls_url":"https://api.github.com/repos/koba-e964/book/pulls{/number}","milestones_url":"https://api.github.com/repos/koba-e964/book/milestones{/number}","notifications_url":"https://api.github.com/repos/koba-e964/book/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/koba-e964/book/labels{/name}","releases_url":"https://api.github.com/repos/koba-e964/book/releases{/id}","deployments_url":"https://api.github.com/repos/koba-e964/book/deployments","created_at":"2016-08-10T04:28:50Z","updated_at":"2016-08-10T04:28:52Z","pushed_at":"2016-10-01T03:06:44Z","git_url":"git://github.com/koba-e964/book.git","ssh_url":"git@github.com:koba-e964/book.git","clone_url":"https://github.com/koba-e964/book.git","svn_url":"https://github.com/koba-e964/book","homepage":null,"size":289284,"stargazers_count":0,"watchers_count":0,"language":"TeX","has_issues":false,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":0,"mirror_url":null,"open_issues_count":0,"forks":0,"open_issues":0,"watchers":0,"default_branch":"master"}},"base":{"label":"HoTT:master","ref":"master","sha":"f706016397da89cb2d82dfaadd24924c70dacb10","user":{"login":"HoTT","id":692156,"avatar_url":"https://avatars.githubusercontent.com/u/692156?v=3","gravatar_id":"","url":"https://api.github.com/users/HoTT","html_url":"https://github.com/HoTT","followers_url":"https://api.github.com/users/HoTT/followers","following_url":"https://api.github.com/users/HoTT/following{/other_user}","gists_url":"https://api.github.com/users/HoTT/gists{/gist_id}","starred_url":"https://api.github.com/users/HoTT/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/HoTT/subscriptions","organizations_url":"https://api.github.com/users/HoTT/orgs","repos_url":"https://api.github.com/users/HoTT/repos","events_url":"https://api.github.com/users/HoTT/events{/privacy}","received_events_url":"https://api.github.com/users/HoTT/received_events","type":"Organization","site_admin":false},"repo":{"id":6569872,"name":"book","full_name":"HoTT/book","owner":{"login":"HoTT","id":692156,"avatar_url":"https://avatars.githubusercontent.com/u/692156?v=3","gravatar_id":"","url":"https://api.github.com/users/HoTT","html_url":"https://github.com/HoTT","followers_url":"https://api.github.com/users/HoTT/followers","following_url":"https://api.github.com/users/HoTT/following{/other_user}","gists_url":"https://api.github.com/users/HoTT/gists{/gist_id}","starred_url":"https://api.github.com/users/HoTT/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/HoTT/subscriptions","organizations_url":"https://api.github.com/users/HoTT/orgs","repos_url":"https://api.github.com/users/HoTT/repos","events_url":"https://api.github.com/users/HoTT/events{/privacy}","received_events_url":"https://api.github.com/users/HoTT/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/HoTT/book","description":"A textbook on informal homotopy type theory","fork":false,"url":"https://api.github.com/repos/HoTT/book","forks_url":"https://api.github.com/repos/HoTT/book/forks","keys_url":"https://api.github.com/repos/HoTT/book/keys{/key_id}","collaborators_url":"https://api.github.com/repos/HoTT/book/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/HoTT/book/teams","hooks_url":"https://api.github.com/repos/HoTT/book/hooks","issue_events_url":"https://api.github.com/repos/HoTT/book/issues/events{/number}","events_url":"https://api.github.com/repos/HoTT/book/events","assignees_url":"https://api.github.com/repos/HoTT/book/assignees{/user}","branches_url":"https://api.github.com/repos/HoTT/book/branches{/branch}","tags_url":"https://api.github.com/repos/HoTT/book/tags","blobs_url":"https://api.github.com/repos/HoTT/book/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/HoTT/book/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/HoTT/book/git/refs{/sha}","trees_url":"https://api.github.com/repos/HoTT/book/git/trees{/sha}","statuses_url":"https://api.github.com/repos/HoTT/book/statuses/{sha}","languages_url":"https://api.github.com/repos/HoTT/book/languages","stargazers_url":"https://api.github.com/repos/HoTT/book/stargazers","contributors_url":"https://api.github.com/repos/HoTT/book/contributors","subscribers_url":"https://api.github.com/repos/HoTT/book/subscribers","subscription_url":"https://api.github.com/repos/HoTT/book/subscription","commits_url":"https://api.github.com/repos/HoTT/book/commits{/sha}","git_commits_url":"https://api.github.com/repos/HoTT/book/git/commits{/sha}","comments_url":"https://api.github.com/repos/HoTT/book/comments{/number}","issue_comment_url":"https://api.github.com/repos/HoTT/book/issues/comments{/number}","contents_url":"https://api.github.com/repos/HoTT/book/contents/{+path}","compare_url":"https://api.github.com/repos/HoTT/book/compare/{base}...{head}","merges_url":"https://api.github.com/repos/HoTT/book/merges","archive_url":"https://api.github.com/repos/HoTT/book/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/HoTT/book/downloads","issues_url":"https://api.github.com/repos/HoTT/book/issues{/number}","pulls_url":"https://api.github.com/repos/HoTT/book/pulls{/number}","milestones_url":"https://api.github.com/repos/HoTT/book/milestones{/number}","notifications_url":"https://api.github.com/repos/HoTT/book/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/HoTT/book/labels{/name}","releases_url":"https://api.github.com/repos/HoTT/book/releases{/id}","deployments_url":"https://api.github.com/repos/HoTT/book/deployments","created_at":"2012-11-06T21:35:02Z","updated_at":"2016-09-28T14:29:24Z","pushed_at":"2016-10-01T03:06:45Z","git_url":"git://github.com/HoTT/book.git","ssh_url":"git@github.com:HoTT/book.git","clone_url":"https://github.com/HoTT/book.git","svn_url":"https://github.com/HoTT/book","homepage":null,"size":341579,"stargazers_count":1063,"watchers_count":1063,"language":"TeX","has_issues":true,"has_downloads":true,"has_wiki":true,"has_pages":true,"forks_count":237,"mirror_url":null,"open_issues_count":52,"forks":237,"open_issues":52,"watchers":1063,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/HoTT/book/pulls/921"},"html":{"href":"https://github.com/HoTT/book/pull/921"},"issue":{"href":"https://api.github.com/repos/HoTT/book/issues/921"},"comments":{"href":"https://api.github.com/repos/HoTT/book/issues/921/comments"},"review_comments":{"href":"https://api.github.com/repos/HoTT/book/pulls/921/comments"},"review_comment":{"href":"https://api.github.com/repos/HoTT/book/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/HoTT/book/pulls/921/commits"},"statuses":{"href":"https://api.github.com/repos/HoTT/book/statuses/c89b3a90e60a83d134aa5545bd42b14046c2e73e"}}}}
{"actor":{"display_login":"koba-e964"}}