{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":763150775,"defaultBranch":"main","name":"poset-type-theory","ownerLogin":"JonasHoefer","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2024-02-25T17:32:43.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/15637557?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1709404792.0","currentOid":""},"activityList":{"items":[{"before":"b573007d41b5ce4f252203fed126f6d9939ce058","after":"56f6c97b782d2ae8cf9f7906c0bb58b48ce8d0d3","ref":"refs/heads/main","pushedAt":"2024-08-19T10:19:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Print sequence of unfolded definition lazily","shortMessageHtmlLink":"Print sequence of unfolded definition lazily"}},{"before":"9a267b3e75580f36483137bd1842e78ef7f0c2f2","after":"b573007d41b5ce4f252203fed126f6d9939ce058","ref":"refs/heads/main","pushedAt":"2024-08-19T10:09:22.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Add `-h` option to hide unfolded term in REPL","shortMessageHtmlLink":"Add <code>-h</code> option to hide unfolded term in REPL"}},{"before":"f14d114d69e2228b54ba1236b16d696d3a806c6b","after":"9a267b3e75580f36483137bd1842e78ef7f0c2f2","ref":"refs/heads/main","pushedAt":"2024-08-19T09:32:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Improve REPL help message for :unfold options","shortMessageHtmlLink":"Improve REPL help message for :unfold options"}},{"before":"90daa4e6d636d33c88f414b770d6177568c5d9a2","after":"f14d114d69e2228b54ba1236b16d696d3a806c6b","ref":"refs/heads/main","pushedAt":"2024-08-19T09:28:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Add option to display head unfolding information sequentially/summed","shortMessageHtmlLink":"Add option to display head unfolding information sequentially/summed"}},{"before":"3d50b2cb2d9e38162c1aef3dfe8307f4b2f7ab5b","after":"90daa4e6d636d33c88f414b770d6177568c5d9a2","ref":"refs/heads/main","pushedAt":"2024-08-18T13:34:29.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Linear unfolding continues unfolding in single argument HIT constructors","shortMessageHtmlLink":"Linear unfolding continues unfolding in single argument HIT constructors"}},{"before":"db21b519e4a15b08be36d18e65fab40b7812d349","after":"3d50b2cb2d9e38162c1aef3dfe8307f4b2f7ab5b","ref":"refs/heads/main","pushedAt":"2024-08-18T12:26:22.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Linear unfolding continuous unfolding single argument HIT constructors","shortMessageHtmlLink":"Linear unfolding continuous unfolding single argument HIT constructors"}},{"before":"1afc34ed60bdfa16df6c1e8875eac5ce795dce6f","after":"db21b519e4a15b08be36d18e65fab40b7812d349","ref":"refs/heads/main","pushedAt":"2024-08-18T12:20:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"More convenient head unfolding in REPL","shortMessageHtmlLink":"More convenient head unfolding in REPL"}},{"before":"e1bbe90429f9627fdf6857eddb30c27ccff805d8","after":"1afc34ed60bdfa16df6c1e8875eac5ce795dce6f","ref":"refs/heads/main","pushedAt":"2024-08-02T14:15:36.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Removed junk file","shortMessageHtmlLink":"Removed junk file"}},{"before":"8b4b734bed55e47afa5c5accf804e4c83b8d4bfd","after":"e1bbe90429f9627fdf6857eddb30c27ccff805d8","ref":"refs/heads/main","pushedAt":"2024-07-17T14:03:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Correct case for `hComp` in inductive type in head linear reduction","shortMessageHtmlLink":"Correct case for <code>hComp</code> in inductive type in head linear reduction"}},{"before":"d416b8d37e92d7777f90eec8c195153e83e28918","after":"8b4b734bed55e47afa5c5accf804e4c83b8d4bfd","ref":"refs/heads/main","pushedAt":"2024-07-16T22:17:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Simplify handling of telescopes","shortMessageHtmlLink":"Simplify handling of telescopes"}},{"before":"32c491d779f458431977a1320b729a5de241f364","after":"d416b8d37e92d7777f90eec8c195153e83e28918","ref":"refs/heads/main","pushedAt":"2024-07-16T22:08:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Fix endpoints in `comp` combinator","shortMessageHtmlLink":"Fix endpoints in <code>comp</code> combinator"}},{"before":"7f5b86ed4caae5abc566a89cadb9374fea52bf3e","after":"32c491d779f458431977a1320b729a5de241f364","ref":"refs/heads/main","pushedAt":"2024-07-16T17:57:02.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Add error for wrong constructor arity in higher splits","shortMessageHtmlLink":"Add error for wrong constructor arity in higher splits"}},{"before":"ffa28fedd79465b6a6b78a893e1240f837dfc373","after":"7f5b86ed4caae5abc566a89cadb9374fea52bf3e","ref":"refs/heads/main","pushedAt":"2024-07-08T11:33:25.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Use `Map` instead of list for scope checking","shortMessageHtmlLink":"Use <code>Map</code> instead of list for scope checking"}},{"before":"e1ac6042a0ae3d55469e27ef9094e8cf5ec80eb3","after":"ffa28fedd79465b6a6b78a893e1240f837dfc373","ref":"refs/heads/main","pushedAt":"2024-06-26T15:40:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Add missing case in scope checker","shortMessageHtmlLink":"Add missing case in scope checker"}},{"before":"c00afc9d20a8056b0629fc8203206d9777aa40c8","after":"e1ac6042a0ae3d55469e27ef9094e8cf5ec80eb3","ref":"refs/heads/main","pushedAt":"2024-06-26T14:58:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Add `hcomp` case for `coe` in HITs","shortMessageHtmlLink":"Add <code>hcomp</code> case for <code>coe</code> in HITs"}},{"before":"f376e5f2acd5e74e9dfcb4339e0dc78880affe66","after":"c00afc9d20a8056b0629fc8203206d9777aa40c8","ref":"refs/heads/main","pushedAt":"2024-06-26T14:48:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Add missing case in quotation","shortMessageHtmlLink":"Add missing case in quotation"}},{"before":"715ab55ccee602915dba1a2aea1321302704daa3","after":"f376e5f2acd5e74e9dfcb4339e0dc78880affe66","ref":"refs/heads/main","pushedAt":"2024-06-26T13:40:16.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Add case for HITs in `doCoePartial`","shortMessageHtmlLink":"Add case for HITs in <code>doCoePartial</code>"}},{"before":"c4a625a93b4b8a93eae7cff8831d0d8096c573ba","after":"715ab55ccee602915dba1a2aea1321302704daa3","ref":"refs/heads/main","pushedAt":"2024-06-26T13:38:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Add case for  in","shortMessageHtmlLink":"Add case for in"}},{"before":"b27a30b33fcb0be3ac87e5b1c9e530af4d16c7f8","after":"c4a625a93b4b8a93eae7cff8831d0d8096c573ba","ref":"refs/heads/main","pushedAt":"2024-06-22T20:15:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Simplify checking of multiple definitions","shortMessageHtmlLink":"Simplify checking of multiple definitions"}},{"before":"5a7a537cd28f4d1eb8e90470d3b6f65e024aad0e","after":"b27a30b33fcb0be3ac87e5b1c9e530af4d16c7f8","ref":"refs/heads/main","pushedAt":"2024-06-20T16:57:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Fix typo in `Prelude.ctt`","shortMessageHtmlLink":"Fix typo in <code>Prelude.ctt</code>"}},{"before":"b4cb8d97a4793cc57da099a3a37cc1b53c4e127e","after":"5a7a537cd28f4d1eb8e90470d3b6f65e024aad0e","ref":"refs/heads/main","pushedAt":"2024-06-20T16:43:38.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Fix reversed environment after type checking","shortMessageHtmlLink":"Fix reversed environment after type checking"}},{"before":"48bd0d30ffef27fa4febfe08df2842125dc4f2cd","after":"b4cb8d97a4793cc57da099a3a37cc1b53c4e127e","ref":"refs/heads/main","pushedAt":"2024-06-19T21:28:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Add `lock` and `unlock` operations similar to `cubicaltt`","shortMessageHtmlLink":"Add <code>lock</code> and <code>unlock</code> operations similar to <code>cubicaltt</code>"}},{"before":"990c425ca29ebb2e17b7a3da584623724caeb267","after":"48bd0d30ffef27fa4febfe08df2842125dc4f2cd","ref":"refs/heads/main","pushedAt":"2024-06-19T17:08:14.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Add missing case to restriction of environment","shortMessageHtmlLink":"Add missing case to restriction of environment"}},{"before":"38cfaf35cd8affa923b8bc283a00e56e00387a3f","after":"990c425ca29ebb2e17b7a3da584623724caeb267","ref":"refs/heads/main","pushedAt":"2024-05-24T16:03:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Fix repl autocompletion for identifiers with non-alphanum idents\n\nAn earlier commit added /, \\, <, and > as valid characters in\nidentifiers. This commit adjusts the repl autocompletion accordingly.","shortMessageHtmlLink":"Fix repl autocompletion for identifiers with non-alphanum idents"}},{"before":"b425178280dcc6a4ad11118e94a299623cf0686e","after":"38cfaf35cd8affa923b8bc283a00e56e00387a3f","ref":"refs/heads/main","pushedAt":"2024-05-23T09:49:31.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Add missing case for stuck `hComp` in `Sum` type in conv. checking","shortMessageHtmlLink":"Add missing case for stuck <code>hComp</code> in <code>Sum</code> type in conv. checking"}},{"before":"12cb841d96cba9f7adade5ee9026c86b2348c1e7","after":"b425178280dcc6a4ad11118e94a299623cf0686e","ref":"refs/heads/main","pushedAt":"2024-05-22T13:49:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Add missing case to `unConSys` used for neutral `hComp`s (closes #3)","shortMessageHtmlLink":"Add missing case to <code>unConSys</code> used for neutral <code>hComp</code>s (<span class=\"issue-keyword tooltipped tooltipped-se\" aria-label=\"This commit closes issue #3.\">closes</span> <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2310506327\" data-permission-text=\"Title is private\" data-url=\"https://github.com/JonasHoefer/poset-type-theory/issues/3\" data-hovercard-type=\"issue\" data-hovercard-url=\"/JonasHoefer/poset-type-theory/issues/3/hovercard\" href=\"https://github.com/JonasHoefer/poset-type-theory/issues/3\">#3</a>)"}},{"before":"f0a59974c4f07c58c6c468a8b7b4718d9f72473b","after":"12cb841d96cba9f7adade5ee9026c86b2348c1e7","ref":"refs/heads/main","pushedAt":"2024-05-20T18:48:45.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Merge pull request #1 from andreasabel/stack\n\nBuild with stack","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2305946986\" data-permission-text=\"Title is private\" data-url=\"https://github.com/JonasHoefer/poset-type-theory/issues/1\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/JonasHoefer/poset-type-theory/pull/1/hovercard\" href=\"https://github.com/JonasHoefer/poset-type-theory/pull/1\">#1</a> from andreasabel/stack"}},{"before":"463e8979dfdccb0a2e26cdf08f593bc9da4c707c","after":"f0a59974c4f07c58c6c468a8b7b4718d9f72473b","ref":"refs/heads/main","pushedAt":"2024-05-09T19:12:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Coe in two variables invariant under permutation of dimensions","shortMessageHtmlLink":"Coe in two variables invariant under permutation of dimensions"}},{"before":"20ca2c123a633cbc524e9a7fc94e77b588936d12","after":"463e8979dfdccb0a2e26cdf08f593bc9da4c707c","ref":"refs/heads/main","pushedAt":"2024-05-08T13:40:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Proof of univalence","shortMessageHtmlLink":"Proof of univalence"}},{"before":"7463f341612c21b65bc9fd238ea58b04c573b22b","after":"20ca2c123a633cbc524e9a7fc94e77b588936d12","ref":"refs/heads/main","pushedAt":"2024-05-06T08:24:53.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"JonasHoefer","name":"Jonas Höfer","path":"/JonasHoefer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15637557?s=80&v=4"},"commit":{"message":"Definition of bi-invertible maps","shortMessageHtmlLink":"Definition of bi-invertible maps"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOC0xOVQxMDoxOToyMy4wMDAwMDBazwAAAASd4zzg","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNS0wNlQwODoyNDo1My4wMDAwMDBazwAAAARCTp-G"}},"title":"Activity · JonasHoefer/poset-type-theory"}