{"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:1717400569.0","currentOid":""},"activityList":{"items":[{"before":"114de4bde86857867773502a3deb1b3e9ad3788d","after":null,"ref":"refs/heads/pi-contract","pushedAt":"2024-06-03T07:42:49.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ncfavier","name":"Naïm Favier","path":"/ncfavier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4323933?s=80&v=4"}},{"before":"699f6de338f4287961a5bfaa48153094853cabc9","after":"b31b1318db2490ed898158653308a56219c80ea9","ref":"refs/heads/gh-pages","pushedAt":"2024-06-03T07:27:58.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@a0b4ba3ed18d16e410d14ab335058509e402cdc2 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ a0b4ba3 🚀"}},{"before":"60f18987bb1819a15fccc325343ef7b469bb2eeb","after":"a0b4ba3ed18d16e410d14ab335058509e402cdc2","ref":"refs/heads/master","pushedAt":"2024-06-03T06:58:17.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":"Add `Π-contractDom` (#1132)","shortMessageHtmlLink":"Add Π-contractDom (#1132)"}},{"before":null,"after":"114de4bde86857867773502a3deb1b3e9ad3788d","ref":"refs/heads/pi-contract","pushedAt":"2024-06-01T09:43:57.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ncfavier","name":"Naïm Favier","path":"/ncfavier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4323933?s=80&v=4"},"commit":{"message":"Add `Π-contractDom`","shortMessageHtmlLink":"Add Π-contractDom"}},{"before":"da6ed74f9cc3ad61741be7c8bc26fae98d0d5778","after":"6c77a131ab2d373db5c08f4379a2257c4da1faa0","ref":"refs/heads/fwellen/no-eta-comm-algebra","pushedAt":"2024-05-31T11:45:56.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":"fix FPAlgebra","shortMessageHtmlLink":"fix FPAlgebra"}},{"before":"984d5772fe4adf98ba72109d869ee68eb17c4fb3","after":"da6ed74f9cc3ad61741be7c8bc26fae98d0d5778","ref":"refs/heads/fwellen/no-eta-comm-algebra","pushedAt":"2024-05-30T14:57:26.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":"fix FPAlgebra","shortMessageHtmlLink":"fix FPAlgebra"}},{"before":"ae141d2ee1fc2c5a74a3eeddd541bbfb0ffc5d69","after":"984d5772fe4adf98ba72109d869ee68eb17c4fb3","ref":"refs/heads/fwellen/no-eta-comm-algebra","pushedAt":"2024-05-30T14:51:45.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":"fix subalgebra","shortMessageHtmlLink":"fix subalgebra"}},{"before":"096708c1195fd7a0231604a68ae8b6399af14a95","after":"ae141d2ee1fc2c5a74a3eeddd541bbfb0ffc5d69","ref":"refs/heads/fwellen/no-eta-comm-algebra","pushedAt":"2024-05-30T12:32:44.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":"fix FreeCommAlg","shortMessageHtmlLink":"fix FreeCommAlg"}},{"before":"a479bab22353f12163407652f654762dec5bed9a","after":"096708c1195fd7a0231604a68ae8b6399af14a95","ref":"refs/heads/fwellen/no-eta-comm-algebra","pushedAt":"2024-05-30T12:17:04.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":"WIP","shortMessageHtmlLink":"WIP"}},{"before":"bc2ee4f46ba0f255ce25608fa8235f9fc1730a4e","after":"699f6de338f4287961a5bfaa48153094853cabc9","ref":"refs/heads/gh-pages","pushedAt":"2024-05-29T14:37:15.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@60f18987bb1819a15fccc325343ef7b469bb2eeb 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ 60f1898 🚀"}},{"before":"502b1bb8a47fb8c07d82e1bc05020d5b4f10cede","after":"60f18987bb1819a15fccc325343ef7b469bb2eeb","ref":"refs/heads/master","pushedAt":"2024-05-29T14:32:58.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":"add lemma to summary file (#1131)","shortMessageHtmlLink":"add lemma to summary file (#1131)"}},{"before":null,"after":"a479bab22353f12163407652f654762dec5bed9a","ref":"refs/heads/fwellen/no-eta-comm-algebra","pushedAt":"2024-05-29T07:54:26.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":"13369aa1190e0e98ea4a25010acf7a185835c9dd","after":"bc2ee4f46ba0f255ce25608fa8235f9fc1730a4e","ref":"refs/heads/gh-pages","pushedAt":"2024-05-22T13:04:10.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@502b1bb8a47fb8c07d82e1bc05020d5b4f10cede 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ 502b1bb 🚀"}},{"before":"2ae84643c74750b49865e44c05b508cb2117c740","after":"502b1bb8a47fb8c07d82e1bc05020d5b4f10cede","ref":"refs/heads/master","pushedAt":"2024-05-22T12:33:50.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":"Simplify CartesianKanOps/FunExtEquiv using \"interpolation\" on I (#1001)\n\n* Simplify CartesianKanOps/FunExtEquiv using \"erp\" interpolation on I\r\n\r\n* Rename \"erp\" to \"interpolateI\"","shortMessageHtmlLink":"Simplify CartesianKanOps/FunExtEquiv using \"interpolation\" on I (#1001)"}},{"before":"e67b457f486fcb2eac00eb41c461f5808690131e","after":"13369aa1190e0e98ea4a25010acf7a185835c9dd","ref":"refs/heads/gh-pages","pushedAt":"2024-05-17T14:16:19.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@2ae84643c74750b49865e44c05b508cb2117c740 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ 2ae8464 🚀"}},{"before":"59c59c00107993c0a7e88307cbc097b4bb7980c6","after":"2ae84643c74750b49865e44c05b508cb2117c740","ref":"refs/heads/master","pushedAt":"2024-05-17T13:42:48.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":"Displayed Category Constructions (#1108)\n\n* Displayed fullsubcategories/preorders/functor introduction principles\r\n\r\nCo-authored-by: Max New \r\n\r\n* Partial definiton of \\exists F (adjoint to reindexing)\r\n\r\n* Remove adjoint to reindex\r\n\r\n* Define left adjoint to reindexing\r\n\r\n* Rename intro for fullsubcategory\r\n\r\n* (Left)AdjontToReindex simplification\r\n\r\n* move intros into separate files, move preorder\r\n\r\n* fstfaithful\r\n\r\n* fix imports\r\n\r\n* Simplify adjoint definition\r\n\r\n* Preorderᴰ > StructureOverC, Fullsubcategoryᴰ > PropertyOverC, clean up imports\r\n\r\n* PropertyOverC > PropertyOver, Weaken to own file, total category moved\r\n\r\n* Fix whitespace + move LeftAdjointToReindex\r\n\r\n* Add left adjoint to reindexing comments\r\n\r\n* expanded comments\r\n\r\n* fix typo\r\n\r\n* isFaithfulFst\r\n\r\n---------\r\n\r\nCo-authored-by: Max New ","shortMessageHtmlLink":"Displayed Category Constructions (#1108)"}},{"before":"d6d640d94cbf3711130e05aed20197bc37621c78","after":"e67b457f486fcb2eac00eb41c461f5808690131e","ref":"refs/heads/gh-pages","pushedAt":"2024-05-14T21:17: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@59c59c00107993c0a7e88307cbc097b4bb7980c6 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ 59c59c0 🚀"}},{"before":"75494455f83698be84857c50de202ec761c5f8d0","after":"59c59c00107993c0a7e88307cbc097b4bb7980c6","ref":"refs/heads/master","pushedAt":"2024-05-14T20:47:03.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":"Clean up: Remove Foundation/Everything and outdated stuff (#1127)\n\n* Clean Codata folder and make it --safe\r\n\r\n* move things around\r\n\r\n* revert\r\n\r\n* remove foundation/everything\r\n\r\n* delete outdated README.md\r\n\r\n* remove Core/Everything, update and clean up imports\r\n\r\n* fix imports\r\n\r\n* fix imports\r\n\r\n* fix imports\r\n\r\n* fix imports\r\n\r\n* fix imports\r\n\r\n---------\r\n\r\nCo-authored-by: Anders Mörtberg ","shortMessageHtmlLink":"Clean up: Remove Foundation/Everything and outdated stuff (#1127)"}},{"before":"0603aadb8964f783ab5d8f7c6ffa95676efd6760","after":"6fd7080d6802d933c53668f159ec043a512c8d1b","ref":"refs/heads/fwellen/no-to-everything","pushedAt":"2024-05-14T19:49:27.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":"fix imports","shortMessageHtmlLink":"fix imports"}},{"before":"4b6a4881840145de3df61f034337f7f6ed0538cb","after":"0603aadb8964f783ab5d8f7c6ffa95676efd6760","ref":"refs/heads/fwellen/no-to-everything","pushedAt":"2024-05-13T15:12:42.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":"fix imports","shortMessageHtmlLink":"fix imports"}},{"before":"404079297b5aee9c3dfd44aa792bef252e19d2db","after":"d6d640d94cbf3711130e05aed20197bc37621c78","ref":"refs/heads/gh-pages","pushedAt":"2024-05-13T14:38:39.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@75494455f83698be84857c50de202ec761c5f8d0 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ 7549445 🚀"}},{"before":"ee26992597f93537b53cf1049f9712733de42957","after":"4b6a4881840145de3df61f034337f7f6ed0538cb","ref":"refs/heads/fwellen/no-to-everything","pushedAt":"2024-05-13T14:24:41.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":"fix imports","shortMessageHtmlLink":"fix imports"}},{"before":"162dd23ea4b63e054715e424d80d0f1901a85295","after":null,"ref":"refs/heads/fwellen/refactor_path_graph","pushedAt":"2024-05-13T14:15:14.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":"9181ef85d9979f849bb37056cd69120861b77b3a","after":"ee26992597f93537b53cf1049f9712733de42957","ref":"refs/heads/fwellen/no-to-everything","pushedAt":"2024-05-13T14:13:51.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":"fix imports","shortMessageHtmlLink":"fix imports"}},{"before":"e956a5bb87260a00cc0f80e90c9d10514d74d047","after":"404079297b5aee9c3dfd44aa792bef252e19d2db","ref":"refs/heads/gh-pages","pushedAt":"2024-05-13T14:10:51.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@542449fa853b640eab5e0f183fed2b32cf0038ea 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ 542449f 🚀"}},{"before":"542449fa853b640eab5e0f183fed2b32cf0038ea","after":"75494455f83698be84857c50de202ec761c5f8d0","ref":"refs/heads/master","pushedAt":"2024-05-13T14:08:41.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":"Simplify `Embedding-into-hLevel→hLevel` (#1107)\n\n* avoid case distinction\r\n\r\n* derive special cases from general statement","shortMessageHtmlLink":"Simplify Embedding-into-hLevel→hLevel (#1107)"}},{"before":"9ec6a593910c8ddaefa9a43e9cbf580ef1675ae1","after":"542449fa853b640eab5e0f183fed2b32cf0038ea","ref":"refs/heads/master","pushedAt":"2024-05-13T14:06:00.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":"Construct 'the' free wild category on a graph (#1117)\n\n* refactor GraphPath, use the same argument order as List in the construction\r\n\r\n* refactor path-graph: make order of arguments more natural, prove coherences\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* tmp\r\n\r\n* choose better name, since it appears in goals\r\n\r\n* define free wild cat and partially define its universal property","shortMessageHtmlLink":"Construct 'the' free wild category on a graph (#1117)"}},{"before":"598d99ae76195367145c1bada1cb0ef9f5de22bf","after":"e956a5bb87260a00cc0f80e90c9d10514d74d047","ref":"refs/heads/gh-pages","pushedAt":"2024-05-13T14:05:35.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@9ec6a593910c8ddaefa9a43e9cbf580ef1675ae1 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ 9ec6a59 🚀"}},{"before":"b046b02b4277f3326daa2be2ba9faa4791f18392","after":"9ec6a593910c8ddaefa9a43e9cbf580ef1675ae1","ref":"refs/heads/master","pushedAt":"2024-05-13T14:01:35.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":"Refactor and extend the path-graph (#1116)\n\n* refactor GraphPath, use the same argument order as List in the construction\r\n\r\n* refactor path-graph: make order of arguments more natural, prove coherences","shortMessageHtmlLink":"Refactor and extend the path-graph (#1116)"}},{"before":"d8b48f638e28677be6f3b87cda3384855a91b502","after":"598d99ae76195367145c1bada1cb0ef9f5de22bf","ref":"refs/heads/gh-pages","pushedAt":"2024-05-13T14:00:13.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@b046b02b4277f3326daa2be2ba9faa4791f18392 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ b046b02 🚀"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEWqYiAgA","startCursor":null,"endCursor":null}},"title":"Activity · agda/cubical"}