{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":602545848,"defaultBranch":"master","name":"agda-unimath","ownerLogin":"VojtechStep","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2023-02-16T12:49:29.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/15523887?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1717604706.0","currentOid":""},"activityList":{"items":[{"before":"227fb7b66c1a6d59f3d851c56b41bf52408498fe","after":"b8af5eb9d48a56076627a687405ba22922d7e056","ref":"refs/heads/feature/warn-zigzag-construction","pushedAt":"2024-06-24T16:07:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Down to one coherence","shortMessageHtmlLink":"Down to one coherence"}},{"before":"1ccb8ec095f8f1e761f83ae8eea8cbfec59763f8","after":"227fb7b66c1a6d59f3d851c56b41bf52408498fe","ref":"refs/heads/feature/warn-zigzag-construction","pushedAt":"2024-06-23T23:18:19.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Down to one hole","shortMessageHtmlLink":"Down to one hole"}},{"before":"2a3bea69fc536a63f961bb792d13e363f064030e","after":"1ccb8ec095f8f1e761f83ae8eea8cbfec59763f8","ref":"refs/heads/feature/warn-zigzag-construction","pushedAt":"2024-06-23T22:21:49.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Some more real progress","shortMessageHtmlLink":"Some more real progress"}},{"before":"f62e861e6043bdc3f6c2d03151d640d4794fe107","after":"2a3bea69fc536a63f961bb792d13e363f064030e","ref":"refs/heads/feature/warn-zigzag-construction","pushedAt":"2024-06-21T12:48:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Progress","shortMessageHtmlLink":"Progress"}},{"before":"5c0ecef51f36b891e980a51c03aa6e4d88332811","after":"f62e861e6043bdc3f6c2d03151d640d4794fe107","ref":"refs/heads/feature/warn-zigzag-construction","pushedAt":"2024-06-14T15:14:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Attempts at coherences","shortMessageHtmlLink":"Attempts at coherences"}},{"before":"76f45078caf54e1f68651ba9f5b870655b6fee9e","after":"5c0ecef51f36b891e980a51c03aa6e4d88332811","ref":"refs/heads/feature/warn-zigzag-construction","pushedAt":"2024-06-13T14:33:56.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Work","shortMessageHtmlLink":"Work"}},{"before":"d4f6a56b7a42ee15b9daba2218ebf55327b0128b","after":"76f45078caf54e1f68651ba9f5b870655b6fee9e","ref":"refs/heads/feature/warn-zigzag-construction","pushedAt":"2024-06-13T14:33:38.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Work","shortMessageHtmlLink":"Work"}},{"before":"a065e506705c5494f2556f4d366db53b7f4f24b3","after":"d4f6a56b7a42ee15b9daba2218ebf55327b0128b","ref":"refs/heads/feature/warn-zigzag-construction","pushedAt":"2024-06-12T16:12:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"WIP interleaved mutual","shortMessageHtmlLink":"WIP interleaved mutual"}},{"before":"09efc0f40ddf53f243ea2c7e7b743b195a6797c4","after":"d2af015fa294356ec521cdfd4f404569829e78c7","ref":"refs/heads/master","pushedAt":"2024-06-08T09:44:38.000Z","pushType":"push","commitsCount":14,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Various website improvements (#1154)\n\n- Renames and moves the \"Formalized results from the literature\"\r\n- Fixes syntax highlighting of Agda flags in the `OPTIONS` pragma\r\n- Fixes #1053 \r\n- Improves line height for #1141","shortMessageHtmlLink":"Various website improvements (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2338609419\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/agda-unimath/issues/1154\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/agda-unimath/pull/1154/hovercard\" href=\"https://github.com/UniMath/agda-unimath/pull/1154\">UniMath#1154</a>)"}},{"before":"20f4ab0ed51a2302aa94034e01d5e08a46a99f30","after":"a065e506705c5494f2556f4d366db53b7f4f24b3","ref":"refs/heads/feature/warn-zigzag-construction","pushedAt":"2024-06-07T16:14:54.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"WIP zigzags identity types","shortMessageHtmlLink":"WIP zigzags identity types"}},{"before":"544423b4260163ec60001878fd2ef362f5bfa03e","after":"20f4ab0ed51a2302aa94034e01d5e08a46a99f30","ref":"refs/heads/feature/warn-zigzag-construction","pushedAt":"2024-06-06T15:58:15.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"WIP zigzags identity types","shortMessageHtmlLink":"WIP zigzags identity types"}},{"before":"f1417c52a5402d7dc760c692229b3d6ce3b653bb","after":"6ea63db0f7731fb510c1688dc8e835834b4a8c4c","ref":"refs/heads/feature/papers-overview","pushedAt":"2024-06-06T15:53:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Improve line height for box-character drawing","shortMessageHtmlLink":"Improve line height for box-character drawing"}},{"before":"cd095b6d0afb35b071d20b8bcbe74e22d9d1e0c7","after":"f1417c52a5402d7dc760c692229b3d6ce3b653bb","ref":"refs/heads/feature/papers-overview","pushedAt":"2024-06-06T15:40:21.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Fix OPTIONS pragma highlighting","shortMessageHtmlLink":"Fix OPTIONS pragma highlighting"}},{"before":"e6fd87897ac5e2cf6c1a33bcd9662000ceb35d99","after":"544423b4260163ec60001878fd2ef362f5bfa03e","ref":"refs/heads/feature/warn-zigzag-construction","pushedAt":"2024-06-05T16:34:12.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"WIP zigzags identity types","shortMessageHtmlLink":"WIP zigzags identity types"}},{"before":"890506951ae6f3a3f5617a1517e1caad691d2bca","after":"db0beed2a4148a8a2240fc57a263be83bb222b7b","ref":"refs/heads/feature/identity-systems-descent-data-pushouts","pushedAt":"2024-06-05T16:33:27.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Fix KvR19 year","shortMessageHtmlLink":"Fix KvR19 year"}},{"before":null,"after":"e6fd87897ac5e2cf6c1a33bcd9662000ceb35d99","ref":"refs/heads/feature/warn-zigzag-construction","pushedAt":"2024-06-05T16:25:06.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"WIP zigzags identity types","shortMessageHtmlLink":"WIP zigzags identity types"}},{"before":"33dcd06f84d911fcb341e38551f50d379583031b","after":"cd095b6d0afb35b071d20b8bcbe74e22d9d1e0c7","ref":"refs/heads/feature/papers-overview","pushedAt":"2024-06-05T14:22:11.000Z","pushType":"push","commitsCount":8,"pusher":{"login":"EgbertRijke","name":"Egbert Rijke","path":"/EgbertRijke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1252282?s=80&v=4"},"commit":{"message":"Merge branch 'master' into feature/papers-overview","shortMessageHtmlLink":"Merge branch 'master' into feature/papers-overview"}},{"before":"927ee994add1cdc704835511754245de87d5c1ce","after":"890506951ae6f3a3f5617a1517e1caad691d2bca","ref":"refs/heads/feature/identity-systems-descent-data-pushouts","pushedAt":"2024-06-05T10:21:30.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Fix KvR19 year","shortMessageHtmlLink":"Fix KvR19 year"}},{"before":"9ce46be522f42323e96cf1ef114001f929e88221","after":"927ee994add1cdc704835511754245de87d5c1ce","ref":"refs/heads/feature/identity-systems-descent-data-pushouts","pushedAt":"2024-06-05T09:04:25.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Fix KvR19 year","shortMessageHtmlLink":"Fix KvR19 year"}},{"before":"c1bb9fb035b7656470b358e963a213c834519dff","after":"9ce46be522f42323e96cf1ef114001f929e88221","ref":"refs/heads/feature/identity-systems-descent-data-pushouts","pushedAt":"2024-06-05T08:54:07.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Fix KvR19 year","shortMessageHtmlLink":"Fix KvR19 year"}},{"before":"45dc92e3879ec48974635614502ec68175097699","after":"c1bb9fb035b7656470b358e963a213c834519dff","ref":"refs/heads/feature/identity-systems-descent-data-pushouts","pushedAt":"2024-06-05T08:52:35.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Fix KvR19 year","shortMessageHtmlLink":"Fix KvR19 year"}},{"before":"27ad4b31f651be727aeee7bbd2f89f3ac051ea09","after":"2b7da8c7114159c033d765696852fe999da0c203","ref":"refs/heads/feature/various-families-over-pushouts","pushedAt":"2024-06-05T07:47:37.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Add a note on the difference between function types and functions","shortMessageHtmlLink":"Add a note on the difference between function types and functions"}},{"before":"e1e5606ac9822779c91cc95790c8b72e113fd3a7","after":"27ad4b31f651be727aeee7bbd2f89f3ac051ea09","ref":"refs/heads/feature/various-families-over-pushouts","pushedAt":"2024-06-04T16:10:04.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Add a note on the difference between function types and functions","shortMessageHtmlLink":"Add a note on the difference between function types and functions"}},{"before":"fe90329c966d239d0ce2d91274f98c8fd3174d7d","after":"e1e5606ac9822779c91cc95790c8b72e113fd3a7","ref":"refs/heads/feature/various-families-over-pushouts","pushedAt":"2024-06-04T15:49:18.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Add a note on the difference between function types and functions","shortMessageHtmlLink":"Add a note on the difference between function types and functions"}},{"before":"874c0c35cf4970b097c68998233adef4b7ba894a","after":"fe90329c966d239d0ce2d91274f98c8fd3174d7d","ref":"refs/heads/feature/various-families-over-pushouts","pushedAt":"2024-06-04T11:43:20.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Parenthesization and `Q` -> `R`","shortMessageHtmlLink":"Parenthesization and <code>Q</code> -&gt; <code>R</code>"}},{"before":"2537cd7af4b080e0269475e8f741036c99fb6c17","after":"45dc92e3879ec48974635614502ec68175097699","ref":"refs/heads/feature/identity-systems-descent-data-pushouts","pushedAt":"2024-06-02T20:40:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Fix KvR19 year","shortMessageHtmlLink":"Fix KvR19 year"}},{"before":"00618b37a8e2f9909aa8ebacf7dee745b8e0fad9","after":"2537cd7af4b080e0269475e8f741036c99fb6c17","ref":"refs/heads/feature/identity-systems-descent-data-pushouts","pushedAt":"2024-06-02T20:10:28.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Descent data as identity systems","shortMessageHtmlLink":"Descent data as identity systems"}},{"before":null,"after":"00618b37a8e2f9909aa8ebacf7dee745b8e0fad9","ref":"refs/heads/feature/identity-systems-descent-data-pushouts","pushedAt":"2024-06-02T19:09:36.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Descent data as identity systems","shortMessageHtmlLink":"Descent data as identity systems"}},{"before":"a39e415a30fa6975370487a918bed804351202dd","after":"874c0c35cf4970b097c68998233adef4b7ba894a","ref":"refs/heads/feature/various-families-over-pushouts","pushedAt":"2024-06-01T16:06:35.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Families of identity types over pushouts","shortMessageHtmlLink":"Families of identity types over pushouts"}},{"before":"b60b0c33bd36b01e38450f04429b2c9a00bb07f9","after":null,"ref":"refs/heads/feature/id-dependent-sequential-diagrams","pushedAt":"2024-06-01T16:05:23.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEbbcmhgA","startCursor":null,"endCursor":null}},"title":"Activity · VojtechStep/agda-unimath"}