{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":153086880,"defaultBranch":"master","name":"cubical","ownerLogin":"agda","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2018-10-15T09:28:28.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/410000?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1711356508.0","currentOid":""},"activityList":{"items":[{"before":"435d1521b46813c4d5d738e422a99432445bb0d3","after":"936b74814274bd1c76a10d4f875a8978076e0fe7","ref":"refs/heads/gh-pages","pushedAt":"2024-05-06T14:56:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/cubical@36a14f8d9be3b4a0eac1e42bdc521381599bacf6 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/cubical/commit/36a14f8d9be3b4a0eac1e42bdc521381599bacf6/hovercard\" href=\"https://github.com/agda/cubical/commit/36a14f8d9be3b4a0eac1e42bdc521381599bacf6\"><tt>36a14f8</tt></a> 🚀"}},{"before":"cb0328e3e7bc4d2dbf375fa8a78f86e78b35bd32","after":"36a14f8d9be3b4a0eac1e42bdc521381599bacf6","ref":"refs/heads/master","pushedAt":"2024-05-06T14:11:25.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mortberg","name":"Anders Mörtberg","path":"/mortberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1068413?s=80&v=4"},"commit":{"message":"CW complexes, cellular homology + a lot more (#1111)\n\n* t\r\n\r\n* duplicate\r\n\r\n* wups\r\n\r\n* rme\r\n\r\n* ganea stuff\r\n\r\n* w\r\n\r\n* w\r\n\r\n* w\r\n\r\n* fix\r\n\r\n* stuff\r\n\r\n* stuff\r\n\r\n* more\r\n\r\n* ..\r\n\r\n* done?\r\n\r\n* wups\r\n\r\n* wups\r\n\r\n* wups\r\n\r\n* fixes\r\n\r\n* ugh...\r\n\r\n* wups\r\n\r\n* stuff\r\n\r\n* stuff\r\n\r\n* stuff\r\n\r\n* stuf\r\n\r\n* More\r\n\r\n* stuff\r\n\r\n* stuff\r\n\r\n* stuff\r\n\r\n* done?\r\n\r\n* stuff\r\n\r\n* cleanup\r\n\r\n* readme\r\n\r\n* wups\r\n\r\n* ugh\r\n\r\n* wups\r\n\r\n* broken code\r\n\r\n* ojdå\r\n\r\n* comments\r\n\r\n* minor","shortMessageHtmlLink":"CW complexes, cellular homology + a lot more (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2165631292\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/cubical/issues/1111\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/cubical/pull/1111/hovercard\" href=\"https://github.com/agda/cubical/pull/1111\">#1111</a>)"}},{"before":"1bdb65d3d1cd27fe43dbc47f37941ffe2731ee36","after":"435d1521b46813c4d5d738e422a99432445bb0d3","ref":"refs/heads/gh-pages","pushedAt":"2024-04-22T09:20:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/cubical@cb0328e3e7bc4d2dbf375fa8a78f86e78b35bd32 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/cubical/commit/cb0328e3e7bc4d2dbf375fa8a78f86e78b35bd32/hovercard\" href=\"https://github.com/agda/cubical/commit/cb0328e3e7bc4d2dbf375fa8a78f86e78b35bd32\"><tt>cb0328e</tt></a> 🚀"}},{"before":"598dfa5c85492f503d04164e79dc4bb0e1e54a24","after":"cb0328e3e7bc4d2dbf375fa8a78f86e78b35bd32","ref":"refs/heads/master","pushedAt":"2024-04-22T09:15:42.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"Preorder structure on the category of subobjects (#1115)\n\n* Update Powerset module\r\n\r\n* Make repeated definition private\r\n\r\n* Remove unnecessary using\r\n\r\n* Sync with agda/cubical\r\n\r\n* Add preorder structure on the category of subobjects","shortMessageHtmlLink":"Preorder structure on the category of subobjects (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2203898854\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/cubical/issues/1115\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/cubical/pull/1115/hovercard\" href=\"https://github.com/agda/cubical/pull/1115\">#1115</a>)"}},{"before":"b824e7830c40d565a3b6a021c1cbf11d7e243a92","after":"1bdb65d3d1cd27fe43dbc47f37941ffe2731ee36","ref":"refs/heads/gh-pages","pushedAt":"2024-04-16T08:42:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/cubical@598dfa5c85492f503d04164e79dc4bb0e1e54a24 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/cubical/commit/598dfa5c85492f503d04164e79dc4bb0e1e54a24/hovercard\" href=\"https://github.com/agda/cubical/commit/598dfa5c85492f503d04164e79dc4bb0e1e54a24\"><tt>598dfa5</tt></a> 🚀"}},{"before":"f9c7655951445ae7a6d277a372946c2b4c9b58c4","after":"598dfa5c85492f503d04164e79dc4bb0e1e54a24","ref":"refs/heads/master","pushedAt":"2024-04-16T08:37:31.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mortberg","name":"Anders Mörtberg","path":"/mortberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1068413?s=80&v=4"},"commit":{"message":"Algebraic geometry directory, take 2 (#1121)\n\n* move Zariski lattice\r\n\r\n* add to README\r\n\r\n* restructure\r\n\r\n* fix paper\r\n\r\n* typos and fixes\r\n\r\n* Z functor instance\r\n\r\n* relative coadjunction","shortMessageHtmlLink":"Algebraic geometry directory, take 2 (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2237801359\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/cubical/issues/1121\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/cubical/pull/1121/hovercard\" href=\"https://github.com/agda/cubical/pull/1121\">#1121</a>)"}},{"before":"9be55256062d03f4cce10aea053386b90b5b261f","after":"b824e7830c40d565a3b6a021c1cbf11d7e243a92","ref":"refs/heads/gh-pages","pushedAt":"2024-04-12T13:12:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/cubical@f9c7655951445ae7a6d277a372946c2b4c9b58c4 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/cubical/commit/f9c7655951445ae7a6d277a372946c2b4c9b58c4/hovercard\" href=\"https://github.com/agda/cubical/commit/f9c7655951445ae7a6d277a372946c2b4c9b58c4\"><tt>f9c7655</tt></a> 🚀"}},{"before":"c26160bec3e8edf3d83597add765a01cc0bf982b","after":"f9c7655951445ae7a6d277a372946c2b4c9b58c4","ref":"refs/heads/master","pushedAt":"2024-04-12T12:28:04.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"Normal form of FreeGroup (#1099)\n\n* nomral form of freegroup and Group solver tactic\r\n\r\n* some cleanup\r\n\r\n* group solver specialised to paths (aware of double-path-composition)\r\n\r\n* fixed name conflict\r\n\r\n* start with boilerplate\r\n\r\n* functor notation\r\n\r\n* free cats\r\n\r\n* write down a candidate def for free wild cat\r\n\r\n* notes\r\n\r\n* wip on grupoidSolver\r\n\r\n* removed solvers\r\n\r\n* removed solvers\r\n\r\n* added brief description of module\r\n\r\n* tweaking comments\r\n\r\n---------\r\n\r\nCo-authored-by: Felix Cherubini <felix.cherubini@posteo.de>","shortMessageHtmlLink":"Normal form of FreeGroup (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2120545851\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/cubical/issues/1099\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/cubical/pull/1099/hovercard\" href=\"https://github.com/agda/cubical/pull/1099\">#1099</a>)"}},{"before":null,"after":"af230159f723a43cc832979ee0f45f018a8ab2cd","ref":"refs/heads/fwellen/free_wild_refl_cat","pushedAt":"2024-03-25T08:48:28.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"wip","shortMessageHtmlLink":"wip"}},{"before":"4ae1de96e7b9ea81a057d32a9b8b9f5155173235","after":"d5bba6740daa7b8940ba7a790631bafa8b724854","ref":"refs/heads/fwellen/try_wild_cat_solver","pushedAt":"2024-03-23T20:26:30.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"define free wild cat and partially define its universal property","shortMessageHtmlLink":"define free wild cat and partially define its universal property"}},{"before":"ae0b2fca3cd84523554d3c048198cfb23aca762a","after":"162dd23ea4b63e054715e424d80d0f1901a85295","ref":"refs/heads/fwellen/refactor_path_graph","pushedAt":"2024-03-23T20:26:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"refactor path-graph: make order of arguments more natural, prove coherences","shortMessageHtmlLink":"refactor path-graph: make order of arguments more natural, prove cohe…"}},{"before":"13859841d85fccb516c3b10233572c1910b9d143","after":"4ae1de96e7b9ea81a057d32a9b8b9f5155173235","ref":"refs/heads/fwellen/try_wild_cat_solver","pushedAt":"2024-03-23T16:55:09.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"tmp","shortMessageHtmlLink":"tmp"}},{"before":null,"after":"ae0b2fca3cd84523554d3c048198cfb23aca762a","ref":"refs/heads/fwellen/refactor_path_graph","pushedAt":"2024-03-23T16:54:02.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"refactor GraphPath, use the same argument order as List in the construction","shortMessageHtmlLink":"refactor GraphPath, use the same argument order as List in the constr…"}},{"before":"fbc6f340aff6f25e338a2d7dd092f2386cd2cb4a","after":"13859841d85fccb516c3b10233572c1910b9d143","ref":"refs/heads/fwellen/try_wild_cat_solver","pushedAt":"2024-03-23T16:16:46.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"write down a candidate def for free wild cat","shortMessageHtmlLink":"write down a candidate def for free wild cat"}},{"before":"c09fcbfebcf60b7fe60e3fa88056eb153d8eb7c7","after":null,"ref":"refs/heads/fwellen/update_agda_version_table","pushedAt":"2024-03-23T14:18:01.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"}},{"before":"cabdab89e03d727419ce28c8b988ca36d89126fd","after":"c26160bec3e8edf3d83597add765a01cc0bf982b","ref":"refs/heads/master","pushedAt":"2024-03-23T10:08:13.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"add latest release (checked locally) (#1114)","shortMessageHtmlLink":"add latest release (checked locally) (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2203797859\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/cubical/issues/1114\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/cubical/pull/1114/hovercard\" href=\"https://github.com/agda/cubical/pull/1114\">#1114</a>)"}},{"before":null,"after":"c09fcbfebcf60b7fe60e3fa88056eb153d8eb7c7","ref":"refs/heads/fwellen/update_agda_version_table","pushedAt":"2024-03-23T09:27:31.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"add latest release (checked locally)","shortMessageHtmlLink":"add latest release (checked locally)"}},{"before":"aec3aaa9769acc6f461c2ac86dba349a46fd6962","after":"9be55256062d03f4cce10aea053386b90b5b261f","ref":"refs/heads/gh-pages","pushedAt":"2024-03-19T06:28:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/cubical@cabdab89e03d727419ce28c8b988ca36d89126fd 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/cubical/commit/cabdab89e03d727419ce28c8b988ca36d89126fd/hovercard\" href=\"https://github.com/agda/cubical/commit/cabdab89e03d727419ce28c8b988ca36d89126fd\"><tt>cabdab8</tt></a> 🚀"}},{"before":"8dc7788d45a45f6420d6290748afb0f343101172","after":"cabdab89e03d727419ce28c8b988ca36d89126fd","ref":"refs/heads/master","pushedAt":"2024-03-19T06:24:03.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mortberg","name":"Anders Mörtberg","path":"/mortberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1068413?s=80&v=4"},"commit":{"message":"papers (#1113)","shortMessageHtmlLink":"papers (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2191666936\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/cubical/issues/1113\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/cubical/pull/1113/hovercard\" href=\"https://github.com/agda/cubical/pull/1113\">#1113</a>)"}},{"before":"475e9e19e78664b656dae4cfd1cd6576baf54ce1","after":"aec3aaa9769acc6f461c2ac86dba349a46fd6962","ref":"refs/heads/gh-pages","pushedAt":"2024-03-16T18:19:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/cubical@8dc7788d45a45f6420d6290748afb0f343101172 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/cubical/commit/8dc7788d45a45f6420d6290748afb0f343101172/hovercard\" href=\"https://github.com/agda/cubical/commit/8dc7788d45a45f6420d6290748afb0f343101172\"><tt>8dc7788</tt></a> 🚀"}},{"before":"fc4ef6a8dd26a2d9b803c8f2f3933464f5171a7b","after":"8dc7788d45a45f6420d6290748afb0f343101172","ref":"refs/heads/master","pushedAt":"2024-03-16T18:06:56.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"Open subschemes (#1096)\n\n* (wip) for Zariski coverage on CommRing\r\n\r\n(with Max Zeuner)\r\n\r\n* pullback stability\r\n\r\n* only zero case left\r\n\r\n* finish zero case\r\n\r\n* def standard affine open\r\n\r\n* finish standard affine opens\r\n\r\n* towards opens of affines\r\n\r\n* discussion\r\n\r\n* little progress\r\n\r\n* towards separatedness\r\n\r\n* separatedness\r\n\r\n* locality\r\n\r\n* towards aff cover\r\n\r\n* give up\r\n\r\n* finish\r\n\r\n* cleanup\r\n\r\n* use inline ring solver\r\n\r\n* fix\r\n\r\n* more fixes\r\n\r\n* fix accidentally public module\r\n\r\nmanually cherry-picked from 93d52b57c6356b209b086fc9752445c05670b59e\r\n\r\n* avoid code duplication\r\n\r\nmanually cherry-picked from 73cc74aba2c0968c987e25d3a5d1855a7e1ec037\r\n\r\n* improve comment\r\n\r\nmanually cherry-picked from 2c4d6d13f1d60ab2cf334cd6a5255b4df418216c\r\n\r\n* slightly improve comment\r\n\r\n* named module StandardOpens\r\n\r\nmanually cherry-picked from d41b1781fcc273fe3445bf10be23e895c29f3939\r\n\r\n* indent by two spaces\r\n\r\n* less whitespace\r\n\r\n* avoid duplication in PosetDownset\r\n\r\n* fix copy-paste errors in comment\r\n\r\n* cleanup JoinMap\r\n\r\n* don't re-prove monoid lemmas\r\n\r\n* slightly clearer comment\r\n\r\n* polish module definition\r\n\r\n* cleanup imports\r\n\r\n* cleanup some more\r\n\r\n* forgotten while renaming ZarMap -> Support\r\n\r\n* upstream 1 lemmas\r\n\r\n* meet map\r\n\r\n---------\r\n\r\nCo-authored-by: Matthias Hutzler <matthias-hutzler@posteo.net>","shortMessageHtmlLink":"Open subschemes (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2112570602\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/cubical/issues/1096\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/cubical/pull/1096/hovercard\" href=\"https://github.com/agda/cubical/pull/1096\">#1096</a>)"}},{"before":"837f35f5a6ce4008edade8b9e25c58910b388459","after":"475e9e19e78664b656dae4cfd1cd6576baf54ce1","ref":"refs/heads/gh-pages","pushedAt":"2024-03-13T12:43:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/cubical@fc4ef6a8dd26a2d9b803c8f2f3933464f5171a7b 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/cubical/commit/fc4ef6a8dd26a2d9b803c8f2f3933464f5171a7b/hovercard\" href=\"https://github.com/agda/cubical/commit/fc4ef6a8dd26a2d9b803c8f2f3933464f5171a7b\"><tt>fc4ef6a</tt></a> 🚀"}},{"before":"6ce70a4934db4dac521c60399183b3b6e1bcf225","after":"fc4ef6a8dd26a2d9b803c8f2f3933464f5171a7b","ref":"refs/heads/master","pushedAt":"2024-03-13T12:13:48.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mortberg","name":"Anders Mörtberg","path":"/mortberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1068413?s=80&v=4"},"commit":{"message":"elimGpd (#1112)\n\n* elimGpd\r\n\r\n* make private","shortMessageHtmlLink":"elimGpd (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2179334239\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/cubical/issues/1112\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/cubical/pull/1112/hovercard\" href=\"https://github.com/agda/cubical/pull/1112\">#1112</a>)"}},{"before":"e295d05f90a2b00b4ecd509221b16b8532b241e6","after":"837f35f5a6ce4008edade8b9e25c58910b388459","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T10:36:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/cubical@6ce70a4934db4dac521c60399183b3b6e1bcf225 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/cubical/commit/6ce70a4934db4dac521c60399183b3b6e1bcf225/hovercard\" href=\"https://github.com/agda/cubical/commit/6ce70a4934db4dac521c60399183b3b6e1bcf225\"><tt>6ce70a4</tt></a> 🚀"}},{"before":"a10e25a8c99efa3b1fee5fa70b8203cd70e88656","after":"6ce70a4934db4dac521c60399183b3b6e1bcf225","ref":"refs/heads/master","pushedAt":"2024-03-01T10:07:32.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mortberg","name":"Anders Mörtberg","path":"/mortberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1068413?s=80&v=4"},"commit":{"message":"Added transportIsoToPath and transportIsoToPath⁻ (#1109)\n\n* Added transportIsoToPath and transportIsoToPath⁻\r\n\r\n* fixed whitespace","shortMessageHtmlLink":"Added transportIsoToPath and transportIsoToPath⁻ (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2162985032\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/cubical/issues/1109\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/cubical/pull/1109/hovercard\" href=\"https://github.com/agda/cubical/pull/1109\">#1109</a>)"}},{"before":"53b0629636c899590ce1b9fb057c682d6008c4bf","after":"a6a41c3e07ea5dfab5851ba9e4f02a7d019fc1ff","ref":"refs/heads/fwellen/free_wild_cats","pushedAt":"2024-03-01T09:11:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"add bigop for wild cats","shortMessageHtmlLink":"add bigop for wild cats"}},{"before":"fa5267b7ee206ee604587ba0eaad58b8caf454e5","after":"e295d05f90a2b00b4ecd509221b16b8532b241e6","ref":"refs/heads/gh-pages","pushedAt":"2024-02-26T08:25:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/cubical@a10e25a8c99efa3b1fee5fa70b8203cd70e88656 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/cubical/commit/a10e25a8c99efa3b1fee5fa70b8203cd70e88656/hovercard\" href=\"https://github.com/agda/cubical/commit/a10e25a8c99efa3b1fee5fa70b8203cd70e88656\"><tt>a10e25a</tt></a> 🚀"}},{"before":"24774d47c1c47a0e57ebb85c07f01ad941df124f","after":"a10e25a8c99efa3b1fee5fa70b8203cd70e88656","ref":"refs/heads/master","pushedAt":"2024-02-26T08:20:06.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"Functorial qcqs-schemes (#1086)\n\n* (wip) for Zariski coverage on CommRing\r\n\r\n(with Max Zeuner)\r\n\r\n* pullback stability\r\n\r\n* 1 ideal lemma\r\n\r\n* only zero case left\r\n\r\n* finish zero case\r\n\r\n* def of scheme\r\n\r\n* renaming\r\n\r\n* cleanup aff sch\r\n\r\n* fixes after review\r\n\r\n* delete zero case\r\n\r\n* some unused imports\r\n\r\n* explanatory comment\r\n\r\n---------\r\n\r\nCo-authored-by: Matthias Hutzler <matthias-hutzler@posteo.net>","shortMessageHtmlLink":"Functorial qcqs-schemes (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2028625825\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/cubical/issues/1086\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/cubical/pull/1086/hovercard\" href=\"https://github.com/agda/cubical/pull/1086\">#1086</a>)"}},{"before":"ba841694370a43879e3ea2718fa656e7747cc787","after":"fa5267b7ee206ee604587ba0eaad58b8caf454e5","ref":"refs/heads/gh-pages","pushedAt":"2024-02-23T10:34:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/cubical@24774d47c1c47a0e57ebb85c07f01ad941df124f 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/cubical/commit/24774d47c1c47a0e57ebb85c07f01ad941df124f/hovercard\" href=\"https://github.com/agda/cubical/commit/24774d47c1c47a0e57ebb85c07f01ad941df124f\"><tt>24774d4</tt></a> 🚀"}},{"before":"d182af36a763d0a354f83650a44e5ac8d5c9726f","after":"24774d47c1c47a0e57ebb85c07f01ad941df124f","ref":"refs/heads/master","pushedAt":"2024-02-23T10:03:52.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"felixwellen","name":"Felix Cherubini","path":"/felixwellen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22154668?s=80&v=4"},"commit":{"message":"Well-orderings and Ordinals (#1072)\n\n* Removed redundant and unused Rel definition\r\n\r\nAlso added the statement that WellFounded is a prop\r\n\r\n* Defined well-orderings\r\n\r\n* Better converting from HoTT's extensionality\r\n\r\n* Moved Woset into its own folder\r\n\r\n* Details on simulations and that WFs are irrefl\r\n\r\n* Proof that well-ordered sets form a poset\r\n\r\n* Constructed well-orderings of an initial segment\r\n\r\n* Changed operator for initial segment\r\n\r\n* Proved the type of well-orders is well-founded\r\n\r\n* Proof that well-orderings are well-ordered\r\n\r\n* Removed unused import\r\n\r\n* Basic properties of well-ordered sets\r\n\r\n* Renamed cardinality to cardinals; defined ordinals\r\n\r\nDefined operations on ordinals;\r\nexponentation remains to be defined.\r\n\r\n* Renamed properties of simulations\r\n\r\n* Changed symbols for ordinal order, started sup\r\n\r\n* Substantial overhaul; better level polymorphism\r\n\r\n* Fix URL\r\n\r\n* Prove properties about ordinal arithmetic\r\n\r\n* Fix missed definition name change\r\n\r\n* Fix whitespace\r\n\r\n* Improved comments as per code review","shortMessageHtmlLink":"Well-orderings and Ordinals (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1966869163\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/cubical/issues/1072\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/cubical/pull/1072/hovercard\" href=\"https://github.com/agda/cubical/pull/1072\">#1072</a>)"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEQqYiKwA","startCursor":null,"endCursor":null}},"title":"Activity · agda/cubical"}