{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":179862204,"defaultBranch":"universal-algebra","name":"UniMath","ownerLogin":"amato-gianluca","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2019-04-06T17:03:52.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/870636?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1707653534.0","currentOid":""},"activityList":{"items":[{"before":"69ecbf1322dfb67cdb5a5dbbe864b22695d2e60b","after":"0b854752e2899d035e733006f474a5e2ffff9146","ref":"refs/heads/master","pushedAt":"2024-02-11T12:06:44.000Z","pushType":"push","commitsCount":5,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"uses Context consistenly (#1841)\n\nThis is nothing but beautification.","shortMessageHtmlLink":"uses Context consistenly (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2125391173\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1841\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1841/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1841\">UniMath#1841</a>)"}},{"before":"cc80340f76f54e43686950b0daba59dda2e04b37","after":"644f5e10d5907ff07ed0a94ab1efd1b00e28e81f","ref":"refs/heads/universal-algebra","pushedAt":"2024-01-31T14:57:28.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"Merge branch 'master' into universal-algebra","shortMessageHtmlLink":"Merge branch 'master' into universal-algebra"}},{"before":"3d6f9db4f92d2e32648d9e53835291a2e06b3085","after":"cc80340f76f54e43686950b0daba59dda2e04b37","ref":"refs/heads/universal-algebra","pushedAt":"2024-01-29T16:40:26.000Z","pushType":"push","commitsCount":10,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Remove output during compilation","shortMessageHtmlLink":"Remove output during compilation"}},{"before":"b1c37590440a6c257ad2fda018aaa5f7466d9750","after":"3d6f9db4f92d2e32648d9e53835291a2e06b3085","ref":"refs/heads/universal-algebra","pushedAt":"2024-01-29T16:39:42.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Proof that axiomatic W-types are initial algebras.","shortMessageHtmlLink":"Proof that axiomatic W-types are initial algebras."}},{"before":"2994aedae76e16736691f9d1deacbb83b21408c3","after":"69ecbf1322dfb67cdb5a5dbbe864b22695d2e60b","ref":"refs/heads/master","pushedAt":"2024-01-29T16:39:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Fix an identifier (#1830)","shortMessageHtmlLink":"Fix an identifier (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2102213985\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1830\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1830/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1830\">UniMath#1830</a>)"}},{"before":"8e1891ee5cad201d27a84c364d35adfd936c9978","after":"6cecc4485986c09d6d0d609bc8cfe4e02859e07e","ref":"refs/heads/coqide-additions","pushedAt":"2024-01-29T16:39:42.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Additions for working in coqide with UniMath.","shortMessageHtmlLink":"Additions for working in coqide with UniMath."}},{"before":"304d94ba14045e0fa46611b7b202322ef7626746","after":"7532963910cf98cee9393ab7f7673d66f7863856","ref":"refs/heads/listne","pushedAt":"2024-01-29T16:39:42.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"First use of non-empty lists for representing terms.","shortMessageHtmlLink":"First use of non-empty lists for representing terms."}},{"before":"3d4d406781832b13a6d07f6361f96497241940c8","after":"cc80340f76f54e43686950b0daba59dda2e04b37","ref":"refs/heads/wtypes","pushedAt":"2024-01-29T16:39:42.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Remove output during compilation","shortMessageHtmlLink":"Remove output during compilation"}},{"before":"d1e70227068d1c1b452dabc1e338a3fda5933772","after":"de05bd33f9d90a49f832ef25fd01b97649101d14","ref":"refs/heads/trees","pushedAt":"2024-01-29T16:39:42.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Trees with prescribed depth.\nUsing wf induction.","shortMessageHtmlLink":"Trees with prescribed depth."}},{"before":"49113b0a8b184cef7cfae896b31eaaf7885154ca","after":"3d4d406781832b13a6d07f6361f96497241940c8","ref":"refs/heads/wtypes","pushedAt":"2024-01-26T17:01:29.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Remove output during compilation","shortMessageHtmlLink":"Remove output during compilation"}},{"before":"5fce0e6e9c96536905c11117b91a25489a770a6d","after":"49113b0a8b184cef7cfae896b31eaaf7885154ca","ref":"refs/heads/wtypes","pushedAt":"2024-01-26T14:57:42.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Update copyright notices for the universal algebra library.","shortMessageHtmlLink":"Update copyright notices for the universal algebra library."}},{"before":"d01ba71a1a643254bfb838b0165244590ed9601a","after":"5fce0e6e9c96536905c11117b91a25489a770a6d","ref":"refs/heads/wtypes","pushedAt":"2024-01-26T12:45:05.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Update copyright notices for the universal algebra library.","shortMessageHtmlLink":"Update copyright notices for the universal algebra library."}},{"before":"d374c5b6b27b15aefcd103fb1b48f298a136baea","after":"d01ba71a1a643254bfb838b0165244590ed9601a","ref":"refs/heads/wtypes","pushedAt":"2024-01-25T14:29:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Update copyright notices for the universal algebra library.","shortMessageHtmlLink":"Update copyright notices for the universal algebra library."}},{"before":"e25f1781a8d8ed06ea3f9726a839cace0547d18c","after":"d374c5b6b27b15aefcd103fb1b48f298a136baea","ref":"refs/heads/wtypes","pushedAt":"2024-01-25T14:22:55.000Z","pushType":"push","commitsCount":10,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"The ground term algebra is a W-type: proof packcaged together","shortMessageHtmlLink":"The ground term algebra is a W-type: proof packcaged together"}},{"before":"c823c93413994ade01705ddf17763662dae7687b","after":"18ee6d8ab63bbcfc488e98acc25654a0ae56a8c7","ref":"refs/heads/singlesorted","pushedAt":"2024-01-25T13:47:01.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"First draft of proof that the term algebra is a W-type.","shortMessageHtmlLink":"First draft of proof that the term algebra is a W-type."}},{"before":"10da5933ccda4e5b398ceca449ed586c2472729d","after":"8e1891ee5cad201d27a84c364d35adfd936c9978","ref":"refs/heads/coqide-additions","pushedAt":"2024-01-25T13:47:01.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Additions for working in coqide with UniMath.","shortMessageHtmlLink":"Additions for working in coqide with UniMath."}},{"before":"a88e8254de70d8d98f4df266d21498e97c3e4b66","after":"304d94ba14045e0fa46611b7b202322ef7626746","ref":"refs/heads/listne","pushedAt":"2024-01-25T09:00:11.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"First use of non-empty lists for representing terms.","shortMessageHtmlLink":"First use of non-empty lists for representing terms."}},{"before":"232ea284aa048e7dd390ede012e7a0e6c1d41e76","after":"b1c37590440a6c257ad2fda018aaa5f7466d9750","ref":"refs/heads/universal-algebra","pushedAt":"2024-01-25T09:00:11.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Proof that axiomatic W-types are initial algebras.","shortMessageHtmlLink":"Proof that axiomatic W-types are initial algebras."}},{"before":"9caec6043d5799873360765ad81877a90727873a","after":"d1e70227068d1c1b452dabc1e338a3fda5933772","ref":"refs/heads/trees","pushedAt":"2024-01-25T09:00:11.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Trees with prescribed depth.\nUsing wf induction.","shortMessageHtmlLink":"Trees with prescribed depth."}},{"before":"5299ee684d0ccfd6deb5c93f58578152a1756aaf","after":"e25f1781a8d8ed06ea3f9726a839cace0547d18c","ref":"refs/heads/wtypes","pushedAt":"2024-01-25T09:00:11.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Initial commit for WTypes.","shortMessageHtmlLink":"Initial commit for WTypes."}},{"before":"5cdc0fe942fd2718e813a4942a94508089ff3504","after":"9caec6043d5799873360765ad81877a90727873a","ref":"refs/heads/trees","pushedAt":"2024-01-25T08:55:24.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Trees with prescribed depth.\nUsing wf induction.","shortMessageHtmlLink":"Trees with prescribed depth."}},{"before":"5b2e2f0988febf47e256d7fc24616e97e099cb25","after":"2994aedae76e16736691f9d1deacbb83b21408c3","ref":"refs/heads/master","pushedAt":"2024-01-25T08:54:34.000Z","pushType":"push","commitsCount":319,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Fix the sanity-checks \"argument list too long\" bug (#1826)\n\n... by moving a large list of files, which was used twice, to a bash\nvariable.","shortMessageHtmlLink":"Fix the sanity-checks \"argument list too long\" bug (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2093712296\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1826\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1826/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1826\">UniMath#1826</a>)"}},{"before":"cb01b21bb012a68e1857f92ea2974608458fa669","after":"5299ee684d0ccfd6deb5c93f58578152a1756aaf","ref":"refs/heads/wtypes","pushedAt":"2024-01-25T08:54:22.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Initial commit for WTypes.","shortMessageHtmlLink":"Initial commit for WTypes."}},{"before":"fb7142638e52fd0b48c6f559dc71707893634733","after":"c823c93413994ade01705ddf17763662dae7687b","ref":"refs/heads/singlesorted","pushedAt":"2023-04-19T13:43:49.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"First draft of proof that the term algebra is a W-type.","shortMessageHtmlLink":"First draft of proof that the term algebra is a W-type."}},{"before":"06c448446b339bc0d29094836cc318bcfc72cdb4","after":"fb7142638e52fd0b48c6f559dc71707893634733","ref":"refs/heads/singlesorted","pushedAt":"2023-04-19T13:21:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Appropriately comment the new lemmas on natural numbers.","shortMessageHtmlLink":"Appropriately comment the new lemmas on natural numbers."}},{"before":"ebc9e5b84f7cb049538afcd1ce1eece8f35d08c4","after":"06c448446b339bc0d29094836cc318bcfc72cdb4","ref":"refs/heads/singlesorted","pushedAt":"2023-04-19T13:16:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Move HVectors to the commun UniMath dir and move there some lemmas.","shortMessageHtmlLink":"Move HVectors to the commun UniMath dir and move there some lemmas."}},{"before":"65a817e8a1cd25e808dcb45f969f6e636f6d9da2","after":"ebc9e5b84f7cb049538afcd1ce1eece8f35d08c4","ref":"refs/heads/singlesorted","pushedAt":"2023-04-19T12:49:49.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Single sorted variant of universal algebra.","shortMessageHtmlLink":"Single sorted variant of universal algebra."}},{"before":"61fb34f5445d35170f3d7c29af4069e119a5a40d","after":"a88e8254de70d8d98f4df266d21498e97c3e4b66","ref":"refs/heads/listne","pushedAt":"2023-04-19T12:47:12.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"First use of non-empty lists for representing terms.","shortMessageHtmlLink":"First use of non-empty lists for representing terms."}},{"before":"75b3f6fb7bffc2bc78ccef437d544c89f4077c6f","after":"5cdc0fe942fd2718e813a4942a94508089ff3504","ref":"refs/heads/trees","pushedAt":"2023-04-19T12:46:54.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Trees with prescribed depth.\nUsing wf induction.","shortMessageHtmlLink":"Trees with prescribed depth."}},{"before":"0a158726e54520e1ae634d63583d601b855cb378","after":"cb01b21bb012a68e1857f92ea2974608458fa669","ref":"refs/heads/wtypes","pushedAt":"2023-04-19T12:46:29.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"amato-gianluca","name":"Gianluca Amato","path":"/amato-gianluca","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/870636?s=80&v=4"},"commit":{"message":"Initial commit for WTypes.","shortMessageHtmlLink":"Initial commit for WTypes."}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wMi0xMVQxMjowNjo0NC4wMDAwMDBazwAAAAP3sc8B","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wMi0xMVQxMjowNjo0NC4wMDAwMDBazwAAAAP3sc8B","endCursor":"Y3Vyc29yOnYyOpK7MjAyMy0wNC0xOVQxMjo0NjoyOS4wMDAwMDBazwAAAAMcATSN"}},"title":"Activity · amato-gianluca/UniMath"}