{"action":"created","comment":{"url":"https://api.github.com/repos/UniMath/UniMath/pulls/comments/78275621","id":78275621,"diff_hunk":"@@ -463,6 +465,88 @@ Defined.\n \n (* Print Assumptions left_adjoint_cocont. *)\n \n+(** Cocontinuity is preserved by isomorphic functors *)\n+Section cocont_iso.\n+\n+Context {C D : precategory} (hsD : has_homsets D) {F G : functor C D} (αiso : @iso [C,D,hsD] F G).\n+\n+Section preserves_colimit_iso.\n+\n+Context {g : graph} (d : diagram g C) (L : C) (cc : cocone d L) (HF : preserves_colimit F d L cc).\n+\n+Let αinv := inv_from_iso αiso.\n+Let α := pr1 αiso.\n+Let Hα : is_iso α := pr2 αiso.\n+\n+Local Definition ccFy y (ccGy : cocone (mapdiagram G d) y) : cocone (mapdiagram F d) y.\n+Proof.\n+use mk_cocone.\n+- intro v; apply (pr1 α (dob d v) ;; coconeIn ccGy v).\n+- abstract (simpl; intros u v e; rewrite <- (coconeInCommutes ccGy u v e), !assoc;\n+            apply cancel_postcomposition, nat_trans_ax).\n+Defined.\n+\n+Lemma αinv_f_commutes y (ccGy : cocone (mapdiagram G d) y) (f : D⟦F L,y⟧)\n+       (Hf : Π v,coconeIn (mapcocone F d cc) v ;; f = coconeIn (ccFy y ccGy) v) :\n+       Π v, # G (coconeIn cc v) ;; (pr1 αinv L ;; f) = coconeIn ccGy v.\n+Proof.\n+intro v; rewrite assoc.\n+eapply pathscomp0; [apply cancel_postcomposition, nat_trans_ax|].\n+rewrite <- assoc; eapply pathscomp0; [apply maponpaths, (Hf v)|]; simpl; rewrite assoc.\n+eapply pathscomp0.\n+  apply cancel_postcomposition.\n+  apply (nat_trans_eq_pointwise (@iso_after_iso_inv [C,D,hsD] _ _ (isopair _ Hα))).\n+now rewrite id_left.\n+Qed.\n+\n+Lemma αinv_f_unique y (ccGy : cocone (mapdiagram G d) y) (f : D⟦F L,y⟧)\n+     (Hf : Π v,coconeIn (mapcocone F d cc) v ;; f = coconeIn (ccFy y ccGy) v)\n+     (HHf : Π t : Σ x, Π v, coconeIn (mapcocone F d cc) v ;; x = coconeIn _ v, t = f,, Hf) :\n+     Π t : Σ x, Π v, # G (coconeIn cc v) ;; x = coconeIn ccGy v,\n+     t = pr1 αinv L ;; f,, αinv_f_commutes y ccGy f Hf.\n+Proof.\n+intros [f' Hf'].\n+apply subtypeEquality; simpl; [intro; apply impred; intro; apply hsD|].\n+transparent assert (HH : (Σ x : D ⟦ F L, y ⟧,\n+            Π v : vertex g,\n+            coconeIn (mapcocone F d cc) v ;; x = coconeIn (ccFy y ccGy) v)).\n+{ mkpair.\n+  - apply (pr1 α L ;; f').\n+  - abstract (intro v; rewrite <- Hf', !assoc; apply cancel_postcomposition, nat_trans_ax).\n+}\n+apply pathsinv0.\n+generalize (maponpaths pr1 (HHf HH)); simpl; intro Htemp.\n+rewrite <- Htemp, assoc.\n+eapply pathscomp0.\n+  apply cancel_postcomposition.\n+  apply (nat_trans_eq_pointwise (@iso_after_iso_inv [C,D,hsD] _ _ (isopair _ Hα))).\n+now apply id_left.\n+Qed.\n+\n+Lemma preserves_colimit_iso  : preserves_colimit G d L cc.\n+Proof.\n+intros HccL y ccGy.\n+set (H := HF HccL y (ccFy y ccGy)).\n+set (f := pr1 (pr1 H)); set (Hf := pr2 (pr1 H)); set (HHf := pr2 H).\n+mkpair.","path":"UniMath/CategoryTheory/CocontFunctors.v","position":189,"original_position":189,"commit_id":"d8f47b08060ed28629ebde41772022eb0b5400f0","original_commit_id":"d8f47b08060ed28629ebde41772022eb0b5400f0","user":{"login":"benediktahrens","id":1106102,"avatar_url":"https://avatars.githubusercontent.com/u/1106102?v=3","gravatar_id":"","url":"https://api.github.com/users/benediktahrens","html_url":"https://github.com/benediktahrens","followers_url":"https://api.github.com/users/benediktahrens/followers","following_url":"https://api.github.com/users/benediktahrens/following{/other_user}","gists_url":"https://api.github.com/users/benediktahrens/gists{/gist_id}","starred_url":"https://api.github.com/users/benediktahrens/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/benediktahrens/subscriptions","organizations_url":"https://api.github.com/users/benediktahrens/orgs","repos_url":"https://api.github.com/users/benediktahrens/repos","events_url":"https://api.github.com/users/benediktahrens/events{/privacy}","received_events_url":"https://api.github.com/users/benediktahrens/received_events","type":"User","site_admin":false},"body":"Also, since what you are proving is a proposition, you can weaken the hypothesis from a specified iso to F and G being isomorphic.\r\nWe don't need this stronger lemma for now, though.","created_at":"2016-09-10T10:57:55Z","updated_at":"2016-09-10T10:57:55Z","html_url":"https://github.com/UniMath/UniMath/pull/456#discussion_r78275621","pull_request_url":"https://api.github.com/repos/UniMath/UniMath/pulls/456","_links":{"self":{"href":"https://api.github.com/repos/UniMath/UniMath/pulls/comments/78275621"},"html":{"href":"https://github.com/UniMath/UniMath/pull/456#discussion_r78275621"},"pull_request":{"href":"https://api.github.com/repos/UniMath/UniMath/pulls/456"}}},"pull_request":{"url":"https://api.github.com/repos/UniMath/UniMath/pulls/456","id":84669250,"html_url":"https://github.com/UniMath/UniMath/pull/456","diff_url":"https://github.com/UniMath/UniMath/pull/456.diff","patch_url":"https://github.com/UniMath/UniMath/pull/456.patch","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/456","number":456,"state":"open","locked":false,"title":"More on cocontinuous functors and (co)limits","user":{"login":"mortberg","id":1068413,"avatar_url":"https://avatars.githubusercontent.com/u/1068413?v=3","gravatar_id":"","url":"https://api.github.com/users/mortberg","html_url":"https://github.com/mortberg","followers_url":"https://api.github.com/users/mortberg/followers","following_url":"https://api.github.com/users/mortberg/following{/other_user}","gists_url":"https://api.github.com/users/mortberg/gists{/gist_id}","starred_url":"https://api.github.com/users/mortberg/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mortberg/subscriptions","organizations_url":"https://api.github.com/users/mortberg/orgs","repos_url":"https://api.github.com/users/mortberg/repos","events_url":"https://api.github.com/users/mortberg/events{/privacy}","received_events_url":"https://api.github.com/users/mortberg/received_events","type":"User","site_admin":false},"body":"This PR contains some new theory about (co)limits and more cleaning:\r\n\r\n* Given two isomorphic functor F and G, if F preserves colimits then G also does. This is then used to drop one of the hypotheses for `is_omega_cocont_binproduct_functor`.\r\n* Generalize assumption for the proofs about `binproduct_pair_functor` and `pair_functor` so that they hold for arbitrary diagrams and not just for chains (this makes it possible to prove that these functors are cocontinuous and not just only omega-cocontinuous).  \r\n* A proof that `isaprop Colims` (and the same for both versions of limits) for univalent/saturated categories. \r\n* More cleaning (more implicit arguments, use tactics like `use`, `mkpair`...)","created_at":"2016-09-09T15:21:27Z","updated_at":"2016-09-10T10:57:55Z","closed_at":null,"merged_at":null,"merge_commit_sha":"35293a035a8b0c587feb9bcf6a6e47ebc4bec810","assignee":null,"assignees":[],"milestone":null,"commits_url":"https://api.github.com/repos/UniMath/UniMath/pulls/456/commits","review_comments_url":"https://api.github.com/repos/UniMath/UniMath/pulls/456/comments","review_comment_url":"https://api.github.com/repos/UniMath/UniMath/pulls/comments{/number}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/456/comments","statuses_url":"https://api.github.com/repos/UniMath/UniMath/statuses/d8f47b08060ed28629ebde41772022eb0b5400f0","head":{"label":"mortberg:generalizecocont","ref":"generalizecocont","sha":"d8f47b08060ed28629ebde41772022eb0b5400f0","user":{"login":"mortberg","id":1068413,"avatar_url":"https://avatars.githubusercontent.com/u/1068413?v=3","gravatar_id":"","url":"https://api.github.com/users/mortberg","html_url":"https://github.com/mortberg","followers_url":"https://api.github.com/users/mortberg/followers","following_url":"https://api.github.com/users/mortberg/following{/other_user}","gists_url":"https://api.github.com/users/mortberg/gists{/gist_id}","starred_url":"https://api.github.com/users/mortberg/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mortberg/subscriptions","organizations_url":"https://api.github.com/users/mortberg/orgs","repos_url":"https://api.github.com/users/mortberg/repos","events_url":"https://api.github.com/users/mortberg/events{/privacy}","received_events_url":"https://api.github.com/users/mortberg/received_events","type":"User","site_admin":false},"repo":{"id":35441413,"name":"UniMath","full_name":"mortberg/UniMath","owner":{"login":"mortberg","id":1068413,"avatar_url":"https://avatars.githubusercontent.com/u/1068413?v=3","gravatar_id":"","url":"https://api.github.com/users/mortberg","html_url":"https://github.com/mortberg","followers_url":"https://api.github.com/users/mortberg/followers","following_url":"https://api.github.com/users/mortberg/following{/other_user}","gists_url":"https://api.github.com/users/mortberg/gists{/gist_id}","starred_url":"https://api.github.com/users/mortberg/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mortberg/subscriptions","organizations_url":"https://api.github.com/users/mortberg/orgs","repos_url":"https://api.github.com/users/mortberg/repos","events_url":"https://api.github.com/users/mortberg/events{/privacy}","received_events_url":"https://api.github.com/users/mortberg/received_events","type":"User","site_admin":false},"private":false,"html_url":"https://github.com/mortberg/UniMath","description":"This coq library aims to formalize a substantial body of mathematics using the univalent point of view.","fork":true,"url":"https://api.github.com/repos/mortberg/UniMath","forks_url":"https://api.github.com/repos/mortberg/UniMath/forks","keys_url":"https://api.github.com/repos/mortberg/UniMath/keys{/key_id}","collaborators_url":"https://api.github.com/repos/mortberg/UniMath/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/mortberg/UniMath/teams","hooks_url":"https://api.github.com/repos/mortberg/UniMath/hooks","issue_events_url":"https://api.github.com/repos/mortberg/UniMath/issues/events{/number}","events_url":"https://api.github.com/repos/mortberg/UniMath/events","assignees_url":"https://api.github.com/repos/mortberg/UniMath/assignees{/user}","branches_url":"https://api.github.com/repos/mortberg/UniMath/branches{/branch}","tags_url":"https://api.github.com/repos/mortberg/UniMath/tags","blobs_url":"https://api.github.com/repos/mortberg/UniMath/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/mortberg/UniMath/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/mortberg/UniMath/git/refs{/sha}","trees_url":"https://api.github.com/repos/mortberg/UniMath/git/trees{/sha}","statuses_url":"https://api.github.com/repos/mortberg/UniMath/statuses/{sha}","languages_url":"https://api.github.com/repos/mortberg/UniMath/languages","stargazers_url":"https://api.github.com/repos/mortberg/UniMath/stargazers","contributors_url":"https://api.github.com/repos/mortberg/UniMath/contributors","subscribers_url":"https://api.github.com/repos/mortberg/UniMath/subscribers","subscription_url":"https://api.github.com/repos/mortberg/UniMath/subscription","commits_url":"https://api.github.com/repos/mortberg/UniMath/commits{/sha}","git_commits_url":"https://api.github.com/repos/mortberg/UniMath/git/commits{/sha}","comments_url":"https://api.github.com/repos/mortberg/UniMath/comments{/number}","issue_comment_url":"https://api.github.com/repos/mortberg/UniMath/issues/comments{/number}","contents_url":"https://api.github.com/repos/mortberg/UniMath/contents/{+path}","compare_url":"https://api.github.com/repos/mortberg/UniMath/compare/{base}...{head}","merges_url":"https://api.github.com/repos/mortberg/UniMath/merges","archive_url":"https://api.github.com/repos/mortberg/UniMath/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/mortberg/UniMath/downloads","issues_url":"https://api.github.com/repos/mortberg/UniMath/issues{/number}","pulls_url":"https://api.github.com/repos/mortberg/UniMath/pulls{/number}","milestones_url":"https://api.github.com/repos/mortberg/UniMath/milestones{/number}","notifications_url":"https://api.github.com/repos/mortberg/UniMath/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/mortberg/UniMath/labels{/name}","releases_url":"https://api.github.com/repos/mortberg/UniMath/releases{/id}","deployments_url":"https://api.github.com/repos/mortberg/UniMath/deployments","created_at":"2015-05-11T18:16:22Z","updated_at":"2016-01-13T19:10:00Z","pushed_at":"2016-09-09T17:45:12Z","git_url":"git://github.com/mortberg/UniMath.git","ssh_url":"git@github.com:mortberg/UniMath.git","clone_url":"https://github.com/mortberg/UniMath.git","svn_url":"https://github.com/mortberg/UniMath","homepage":"","size":10127,"stargazers_count":0,"watchers_count":0,"language":"Coq","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":"UniMath:master","ref":"master","sha":"149cedd12d9ff4ba95040662f2a09e6e076b696d","user":{"login":"UniMath","id":6826454,"avatar_url":"https://avatars.githubusercontent.com/u/6826454?v=3","gravatar_id":"","url":"https://api.github.com/users/UniMath","html_url":"https://github.com/UniMath","followers_url":"https://api.github.com/users/UniMath/followers","following_url":"https://api.github.com/users/UniMath/following{/other_user}","gists_url":"https://api.github.com/users/UniMath/gists{/gist_id}","starred_url":"https://api.github.com/users/UniMath/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/UniMath/subscriptions","organizations_url":"https://api.github.com/users/UniMath/orgs","repos_url":"https://api.github.com/users/UniMath/repos","events_url":"https://api.github.com/users/UniMath/events{/privacy}","received_events_url":"https://api.github.com/users/UniMath/received_events","type":"Organization","site_admin":false},"repo":{"id":17321421,"name":"UniMath","full_name":"UniMath/UniMath","owner":{"login":"UniMath","id":6826454,"avatar_url":"https://avatars.githubusercontent.com/u/6826454?v=3","gravatar_id":"","url":"https://api.github.com/users/UniMath","html_url":"https://github.com/UniMath","followers_url":"https://api.github.com/users/UniMath/followers","following_url":"https://api.github.com/users/UniMath/following{/other_user}","gists_url":"https://api.github.com/users/UniMath/gists{/gist_id}","starred_url":"https://api.github.com/users/UniMath/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/UniMath/subscriptions","organizations_url":"https://api.github.com/users/UniMath/orgs","repos_url":"https://api.github.com/users/UniMath/repos","events_url":"https://api.github.com/users/UniMath/events{/privacy}","received_events_url":"https://api.github.com/users/UniMath/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/UniMath/UniMath","description":"This coq library aims to formalize a substantial body of mathematics using the univalent point of view.","fork":false,"url":"https://api.github.com/repos/UniMath/UniMath","forks_url":"https://api.github.com/repos/UniMath/UniMath/forks","keys_url":"https://api.github.com/repos/UniMath/UniMath/keys{/key_id}","collaborators_url":"https://api.github.com/repos/UniMath/UniMath/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/UniMath/UniMath/teams","hooks_url":"https://api.github.com/repos/UniMath/UniMath/hooks","issue_events_url":"https://api.github.com/repos/UniMath/UniMath/issues/events{/number}","events_url":"https://api.github.com/repos/UniMath/UniMath/events","assignees_url":"https://api.github.com/repos/UniMath/UniMath/assignees{/user}","branches_url":"https://api.github.com/repos/UniMath/UniMath/branches{/branch}","tags_url":"https://api.github.com/repos/UniMath/UniMath/tags","blobs_url":"https://api.github.com/repos/UniMath/UniMath/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/UniMath/UniMath/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/UniMath/UniMath/git/refs{/sha}","trees_url":"https://api.github.com/repos/UniMath/UniMath/git/trees{/sha}","statuses_url":"https://api.github.com/repos/UniMath/UniMath/statuses/{sha}","languages_url":"https://api.github.com/repos/UniMath/UniMath/languages","stargazers_url":"https://api.github.com/repos/UniMath/UniMath/stargazers","contributors_url":"https://api.github.com/repos/UniMath/UniMath/contributors","subscribers_url":"https://api.github.com/repos/UniMath/UniMath/subscribers","subscription_url":"https://api.github.com/repos/UniMath/UniMath/subscription","commits_url":"https://api.github.com/repos/UniMath/UniMath/commits{/sha}","git_commits_url":"https://api.github.com/repos/UniMath/UniMath/git/commits{/sha}","comments_url":"https://api.github.com/repos/UniMath/UniMath/comments{/number}","issue_comment_url":"https://api.github.com/repos/UniMath/UniMath/issues/comments{/number}","contents_url":"https://api.github.com/repos/UniMath/UniMath/contents/{+path}","compare_url":"https://api.github.com/repos/UniMath/UniMath/compare/{base}...{head}","merges_url":"https://api.github.com/repos/UniMath/UniMath/merges","archive_url":"https://api.github.com/repos/UniMath/UniMath/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/UniMath/UniMath/downloads","issues_url":"https://api.github.com/repos/UniMath/UniMath/issues{/number}","pulls_url":"https://api.github.com/repos/UniMath/UniMath/pulls{/number}","milestones_url":"https://api.github.com/repos/UniMath/UniMath/milestones{/number}","notifications_url":"https://api.github.com/repos/UniMath/UniMath/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/UniMath/UniMath/labels{/name}","releases_url":"https://api.github.com/repos/UniMath/UniMath/releases{/id}","deployments_url":"https://api.github.com/repos/UniMath/UniMath/deployments","created_at":"2014-03-01T18:37:12Z","updated_at":"2016-09-10T04:03:56Z","pushed_at":"2016-09-10T10:00:52Z","git_url":"git://github.com/UniMath/UniMath.git","ssh_url":"git@github.com:UniMath/UniMath.git","clone_url":"https://github.com/UniMath/UniMath.git","svn_url":"https://github.com/UniMath/UniMath","homepage":"","size":11204,"stargazers_count":164,"watchers_count":164,"language":"Coq","has_issues":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":34,"mirror_url":null,"open_issues_count":61,"forks":34,"open_issues":61,"watchers":164,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/UniMath/UniMath/pulls/456"},"html":{"href":"https://github.com/UniMath/UniMath/pull/456"},"issue":{"href":"https://api.github.com/repos/UniMath/UniMath/issues/456"},"comments":{"href":"https://api.github.com/repos/UniMath/UniMath/issues/456/comments"},"review_comments":{"href":"https://api.github.com/repos/UniMath/UniMath/pulls/456/comments"},"review_comment":{"href":"https://api.github.com/repos/UniMath/UniMath/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/UniMath/UniMath/pulls/456/commits"},"statuses":{"href":"https://api.github.com/repos/UniMath/UniMath/statuses/d8f47b08060ed28629ebde41772022eb0b5400f0"}}}}
{"actor":{"display_login":"benediktahrens"}}