{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":69886214,"defaultBranch":"master","name":"TypeTheory","ownerLogin":"UniMath","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2016-10-03T15:54:42.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/6826454?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1653919669.149703","currentOid":""},"activityList":{"items":[{"before":"d6f8dcad8efe4794a0dfa45630a7718b1bd1e442","after":"039a6bcaa653dd8c3dc377c757f29bb13ff6a19f","ref":"refs/heads/master","pushedAt":"2024-02-08T19:04:33.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"rmatthes","name":"Ralph Matthes","path":"/rmatthes","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12064214?s=80&v=4"},"commit":{"message":"Merge pull request #244 from rmatthes/githubactionsv4\n\nGitHub action v3 -> v4, Dune language 3.5 -> 3.8, Coq language 0.6 -> 0.8","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2123967560\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/TypeTheory/issues/244\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/TypeTheory/pull/244/hovercard\" href=\"https://github.com/UniMath/TypeTheory/pull/244\">#244</a> from rmatthes/githubactionsv4"}},{"before":"c506b8f44d0c7892ab5489d5faf4b6deb42aa62c","after":"d6f8dcad8efe4794a0dfa45630a7718b1bd1e442","ref":"refs/heads/master","pushedAt":"2024-02-07T17:57:32.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"rmatthes","name":"Ralph Matthes","path":"/rmatthes","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12064214?s=80&v=4"},"commit":{"message":"Merge pull request #243 from arnoudvanderleer/rename-category-packages\n\nUpdate references to category packages","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2122934809\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/TypeTheory/issues/243\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/TypeTheory/pull/243/hovercard\" href=\"https://github.com/UniMath/TypeTheory/pull/243\">#243</a> from arnoudvanderleer/rename-category-packages"}},{"before":"3dfd6013aa4f15bc266c2a05bd8dd53538a417f7","after":"c506b8f44d0c7892ab5489d5faf4b6deb42aa62c","ref":"refs/heads/master","pushedAt":"2024-01-30T15:43:37.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"Merge pull request #242 from rmatthes/followupstreamPR1829\n\nrestores compilation after UniMath PR1829","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2100964701\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/TypeTheory/issues/242\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/TypeTheory/pull/242/hovercard\" href=\"https://github.com/UniMath/TypeTheory/pull/242\">#242</a> from rmatthes/followupstreamPR1829"}},{"before":"7205f8bd15b7644ad81a33c48f0cd1398b8d486c","after":"3dfd6013aa4f15bc266c2a05bd8dd53538a417f7","ref":"refs/heads/master","pushedAt":"2023-08-29T14:58:08.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"rmatthes","name":"Ralph Matthes","path":"/rmatthes","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12064214?s=80&v=4"},"commit":{"message":"Merge pull request #241 from rmatthes/restorecompafterunimathPR1768\n\nupstream change to is_univalent_full_sub_category","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1871828849\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/TypeTheory/issues/241\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/TypeTheory/pull/241/hovercard\" href=\"https://github.com/UniMath/TypeTheory/pull/241\">#241</a> from rmatthes/restorecompafterunimathPR1768"}},{"before":"2479a7f7b7efd2da444e34e1b76e00a9c63a6baf","after":"7205f8bd15b7644ad81a33c48f0cd1398b8d486c","ref":"refs/heads/master","pushedAt":"2023-08-16T14:49:13.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"Merge pull request #240 from rmatthes/restorecompilationafterUniMathPR1756\n\nrestores compilation after upstream PR#1756","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1853382098\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/TypeTheory/issues/240\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/TypeTheory/pull/240/hovercard\" href=\"https://github.com/UniMath/TypeTheory/pull/240\">#240</a> from rmatthes/restorecompilationafterUniMathP…"}},{"before":"b2aa8ef0fc3c292e3fb2614482e03051273ce861","after":"2479a7f7b7efd2da444e34e1b76e00a9c63a6baf","ref":"refs/heads/master","pushedAt":"2023-06-25T19:45:47.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"Merge pull request #238 from Skantz/initlogic\n\n#235: Remove dependency on Coq.Init.Logic","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1772665086\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/TypeTheory/issues/238\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/TypeTheory/pull/238/hovercard\" href=\"https://github.com/UniMath/TypeTheory/pull/238\">#238</a> from Skantz/initlogic"}},{"before":"f18bbdf5661c389e9de43c6d800ef1528ffbea32","after":"b2aa8ef0fc3c292e3fb2614482e03051273ce861","ref":"refs/heads/master","pushedAt":"2023-05-21T21:07:39.555Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"peterlefanulumsdaine","name":"Peter LeFanu Lumsdaine","path":"/peterlefanulumsdaine","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/295280?s=80&v=4"},"commit":{"message":"Merge pull request #237 from peterlefanulumsdaine/set-univ-checking\n\nReplace `-type-in-type` with `Unset Universe Checking`","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1718632533\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/TypeTheory/issues/237\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/TypeTheory/pull/237/hovercard\" href=\"https://github.com/UniMath/TypeTheory/pull/237\">#237</a> from peterlefanulumsdaine/set-univ-checking"}},{"before":"e7fc5a0c4564afc44b084d134e4110d447b68404","after":"f18bbdf5661c389e9de43c6d800ef1528ffbea32","ref":"refs/heads/master","pushedAt":"2023-04-03T16:09:21.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"m-lindgren","name":"Michael Lindgren","path":"/m-lindgren","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/29382325?s=80&v=4"},"commit":{"message":"Workaround Coq bug.\n\nRecent coq-dev breaks on TypeTheory. This is reported as\nCoq issue #17461.\n\nThis commit also changes CI to build TypeTheory with coq-dev,\nso that we can verify this workaround.","shortMessageHtmlLink":"Workaround Coq bug."}},{"before":"8fab18e6f9c47a31b88f825a0de31fe9e96e8448","after":"e7fc5a0c4564afc44b084d134e4110d447b68404","ref":"refs/heads/master","pushedAt":"2023-03-07T20:57:02.000Z","pushType":"pr_merge","commitsCount":6,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"Merge pull request #234 from m-lindgren/tt-remove-coq-init\n\nRemove or make explicit dependency on coq.init.logic","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1610283887\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/TypeTheory/issues/234\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/TypeTheory/pull/234/hovercard\" href=\"https://github.com/UniMath/TypeTheory/pull/234\">#234</a> from m-lindgren/tt-remove-coq-init"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAD9dl1cAA","startCursor":null,"endCursor":null}},"title":"Activity · UniMath/TypeTheory"}