{"action":"created","comment":{"url":"https://api.github.com/repos/UniMath/UniMath/pulls/comments/77901962","id":77901962,"diff_hunk":"@@ -78,75 +82,514 @@ Require Import UniMath.CategoryTheory.CommaCategories.\n Local Notation \"# F\" := (functor_on_morphisms F) (at level 3).\n Local Notation \"[ C , D , hs ]\" := (functor_precategory C D hs).\n \n-Section move_upstream.\n+(** * Definition of cocontinuous functors *)\n+Section cocont.\n+\n+Context {C D : precategory} (F : functor C D).\n+\n+Definition mapdiagram {g : graph} (d : diagram g C) : diagram g D.\n+Proof.\n+simple refine (tpair _ _ _).\n+- intros n.\n+  apply (F (dob d n)).\n+- simpl; intros m n e.\n+  apply (# F (dmor d e)).\n+Defined.\n+\n+Definition mapcocone {g : graph} (d : diagram g C) {x : C}\n+  (dx : cocone d x) : cocone (mapdiagram d) (F x).\n+Proof.\n+simple refine (mk_cocone _ _).\n+- simpl; intro n.\n+  exact (#F (coconeIn dx n)).\n+- abstract (intros u v e; simpl; rewrite <- functor_comp;\n+            apply maponpaths, (coconeInCommutes dx _ _ e)).\n+Defined.\n+\n+Lemma mapcocone_chain_coconeIn {g : graph} {c : diagram g C} {x : C}\n+  (cx : cocone c x) (n : vertex g) :\n+  coconeIn (mapcocone c cx) n = # F (coconeIn cx n).\n+Proof.\n+apply idpath.\n+Qed.\n+\n+Definition preserves_colimits {g : graph} (d : diagram g C) (L : C)\n+  (cc : cocone d L) : UU :=\n+  isColimCocone d L cc -> isColimCocone (mapdiagram d) (F L) (mapcocone d cc).\n+\n+Definition is_cocont := Π {g : graph} (d : diagram g C) (L : C)\n+  (cc : cocone d L), preserves_colimits d L cc.\n \n-Lemma paireta {A B : UU} (p : A × B) : p = (pr1 p,, pr2 p).\n+End cocont.\n+\n+(** * Definition of chains and omega-cocontinuous functors *)\n+Section omega_cocont.\n+\n+(** Define the chain:\n+\n+     0 --> 1 --> 2 --> 3 --> ...\n+\n+   with exactly one arrow from n to S n.\n+*)\n+Definition nat_graph : graph :=\n+  tpair (λ D : UU, D → D → UU) nat (λ m n, S m = n).\n+\n+Local Notation \"'chain'\" := (diagram nat_graph).\n+\n+Definition mapchain {C D : precategory} (F : functor C D)\n+  (c : chain C) : chain D := mapdiagram F c.\n+\n+(** Any i < j gives a morphism in the chain *)\n+Definition chain_mor {C : precategory} (c : chain C) {i j} :\n+  i < j -> C⟦dob c i, dob c j⟧.\n Proof.\n-destruct p; apply idpath.\n+induction j.\n+- intros Hi0.\n+  destruct (negnatlthn0 0 Hi0).\n+- intros Hij.\n+  destruct (natlehchoice4 _ _ Hij) as [|H].\n+  + apply (IHj h ;; dmor c (idpath (S j))).\n+  + apply dmor, (maponpaths S H).\n Defined.\n \n-End move_upstream.\n+Lemma chain_mor_coconeIn {C : precategory} (c : chain C) (x : C)\n+  (cc : cocone c x) i : Π j (Hij : i < j),\n+  chain_mor c Hij ;; coconeIn cc j = coconeIn cc i.\n+Proof.\n+induction j.\n+- intros Hi0.\n+  destruct (negnatlthn0 _ Hi0).\n+- intros Hij; simpl.\n+  destruct (natlehchoice4 _ _ Hij).\n+  + rewrite <- (IHj h), <- assoc.\n+    apply maponpaths, coconeInCommutes.\n+  + destruct p.\n+    apply coconeInCommutes.\n+Qed.\n+\n+Lemma chain_mor_right {C : precategory} {c : chain C} {i j} (Hij : i < j) (HSij : S i < j) :\n+  dmor c (idpath (S i)) ;; chain_mor c HSij = chain_mor c Hij.\n+Proof.\n+induction j.\n+- destruct (negnatlthn0 _ Hij).\n+- simpl.\n+  destruct (natlehchoice4 _ _ Hij).\n+  + destruct (natlehchoice4 _ _ HSij).\n+    * now rewrite <- (IHj h h0), assoc.\n+    * destruct p; simpl.\n+      destruct (natlehchoice4 _ _ h); [destruct (isirreflnatlth _ h0)|].\n+      apply cancel_postcomposition, maponpaths, isasetnat.\n+  + destruct p, (isirreflnatlth _ HSij).\n+Qed.\n+\n+Lemma chain_mor_left {C : precategory} {c : chain C} {i j} (Hij : i < j) (HiSj : i < S j) :\n+  chain_mor c Hij ;; dmor c (idpath (S j)) = chain_mor c HiSj.\n+Proof.\n+destruct j.\n+- destruct (negnatlthn0 _ Hij).\n+- simpl; destruct (natlehchoice4 i (S j) HiSj).\n+  + destruct (natlehchoice4 _ _ h).\n+    * destruct (natlehchoice4 _ _ Hij); [|destruct p, (isirreflnatlth _ h0)].\n+      apply cancel_postcomposition, cancel_postcomposition, maponpaths, isasetbool.\n+    * destruct p; simpl.\n+      destruct (natlehchoice4 _ _ Hij); [destruct (isirreflnatlth _ h0)|].\n+      apply cancel_postcomposition, maponpaths, isasetnat.\n+  + generalize Hij; rewrite p; intros H.\n+    destruct (isirreflnatlth _ H).\n+Qed.\n+\n+(** Construct the initial chain:\n+\n+         !          F!            F^2 !\n+     0 -----> F 0 ------> F^2 0 --------> F^3 0 ---> ...\n+\n+*)\n+Definition initChain {C : precategory} (InitC : Initial C) (F : functor C C) : chain C.\n+Proof.\n+exists (λ n, iter_functor F n InitC).\n+intros m n Hmn. destruct Hmn. simpl.\n+induction m as [|m IHm]; simpl.\n+- exact (InitialArrow InitC _).\n+- exact (# F IHm).\n+Defined.\n+\n+Definition is_omega_cocont {C D : precategory} (F : functor C D) : UU :=\n+  Π (c : chain C) (L : C) (cc : cocone c L),\n+  preserves_colimits F c L cc.\n+\n+Definition omega_cocont_functor (C D : precategory) : UU :=\n+  Σ (F : functor C D), is_omega_cocont F.\n+\n+End omega_cocont.\n+\n+Local Notation \"'chain'\" := (diagram nat_graph).\n+\n+\n+(** * Adámek's theorem for constructing initial algebras of omega-cocontinuous functors *)\n+(* This section proves that (L,α : F L -> L) is the initial algebra\n+    where L is the colimit of the inital chain:\n+\n+         !          F !           F^2 !\n+     0 -----> F 0 ------> F^2 0 --------> F^3 0 ---> ...\n+\n+This result is also known as Adámek's theorem:\n+\n+  https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor#AdameksTheorem","path":"UniMath/CategoryTheory/CocontFunctors.v","position":213,"original_position":213,"commit_id":"7a07d92bdc60988a135b1f92c59974ffbed20ac7","original_commit_id":"7a07d92bdc60988a135b1f92c59974ffbed20ac7","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":"Could you insert a reference to Adamek's article here, as discussed in #316 ?","created_at":"2016-09-07T20:55:10Z","updated_at":"2016-09-07T20:55:10Z","html_url":"https://github.com/UniMath/UniMath/pull/451#discussion_r77901962","pull_request_url":"https://api.github.com/repos/UniMath/UniMath/pulls/451","_links":{"self":{"href":"https://api.github.com/repos/UniMath/UniMath/pulls/comments/77901962"},"html":{"href":"https://github.com/UniMath/UniMath/pull/451#discussion_r77901962"},"pull_request":{"href":"https://api.github.com/repos/UniMath/UniMath/pulls/451"}}},"pull_request":{"url":"https://api.github.com/repos/UniMath/UniMath/pulls/451","id":84369884,"html_url":"https://github.com/UniMath/UniMath/pull/451","diff_url":"https://github.com/UniMath/UniMath/pull/451.diff","patch_url":"https://github.com/UniMath/UniMath/pull/451.patch","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/451","number":451,"state":"open","locked":false,"title":"Clean cocontinuous functors","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 cleans the formalization of cocontinuous functors by:\r\n\r\n* Merge all the theory about cocontinuous functors into CocontFunctors.v\r\n* Add more documentation and make HTML output nicer\r\n* Weaken a hypothesis of is_omega_cocont_binproduct_functor as suggested by Benedikt (this will be improved further in a future PR)\r\n* Lots of cleaning, get rid of some `match`'s and add `Local` to some Definitions","created_at":"2016-09-07T20:42:20Z","updated_at":"2016-09-07T20:55:10Z","closed_at":null,"merged_at":null,"merge_commit_sha":"bffec9329685fe570410cb9ca1346d515a28ab2a","assignee":null,"assignees":[],"milestone":null,"commits_url":"https://api.github.com/repos/UniMath/UniMath/pulls/451/commits","review_comments_url":"https://api.github.com/repos/UniMath/UniMath/pulls/451/comments","review_comment_url":"https://api.github.com/repos/UniMath/UniMath/pulls/comments{/number}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/451/comments","statuses_url":"https://api.github.com/repos/UniMath/UniMath/statuses/7a07d92bdc60988a135b1f92c59974ffbed20ac7","head":{"label":"mortberg:cleancocont","ref":"cleancocont","sha":"7a07d92bdc60988a135b1f92c59974ffbed20ac7","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-07T20:33:15Z","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":10002,"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":"1fba1802ed2ff5cde9fef20b96ad8f3d21ea04f2","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-08-22T22:16:37Z","pushed_at":"2016-09-07T20:43:58Z","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":11031,"stargazers_count":162,"watchers_count":162,"language":"Coq","has_issues":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":34,"mirror_url":null,"open_issues_count":72,"forks":34,"open_issues":72,"watchers":162,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/UniMath/UniMath/pulls/451"},"html":{"href":"https://github.com/UniMath/UniMath/pull/451"},"issue":{"href":"https://api.github.com/repos/UniMath/UniMath/issues/451"},"comments":{"href":"https://api.github.com/repos/UniMath/UniMath/issues/451/comments"},"review_comments":{"href":"https://api.github.com/repos/UniMath/UniMath/pulls/451/comments"},"review_comment":{"href":"https://api.github.com/repos/UniMath/UniMath/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/UniMath/UniMath/pulls/451/commits"},"statuses":{"href":"https://api.github.com/repos/UniMath/UniMath/statuses/7a07d92bdc60988a135b1f92c59974ffbed20ac7"}}}}
{"actor":{"display_login":"benediktahrens"}}