{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":368006528,"defaultBranch":"master","name":"Type-Theory-Wishlist","ownerLogin":"wkolowski","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2021-05-16T23:35:08.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/3518202?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1621473445.2218938","currentOid":""},"activityList":{"items":[{"before":"2adc55df92f835661e99851853433ee461dbbcd3","after":"0bbd5198705deadba69ecf522ea947cf610caf98","ref":"refs/heads/master","pushedAt":"2024-07-12T13:38:56.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"wkolowski","name":"Wojciech Kołowski","path":"/wkolowski","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3518202?s=80&v=4"},"commit":{"message":"Universe of definitionally decidable propositions (note in Polish).","shortMessageHtmlLink":"Universe of definitionally decidable propositions (note in Polish)."}},{"before":"1a2af7483842b699e5eb8d4e6d9f65a63694464e","after":"2adc55df92f835661e99851853433ee461dbbcd3","ref":"refs/heads/master","pushedAt":"2024-04-05T01:36:57.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"wkolowski","name":"Wojciech Kołowski","path":"/wkolowski","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3518202?s=80&v=4"},"commit":{"message":"An example of a non-trivial use of subtyping for variants.","shortMessageHtmlLink":"An example of a non-trivial use of subtyping for variants."}},{"before":"d1b39c6465fd2e450056eb3622e4321fd3e32b54","after":"1a2af7483842b699e5eb8d4e6d9f65a63694464e","ref":"refs/heads/master","pushedAt":"2024-04-02T01:09:24.000Z","pushType":"push","commitsCount":14,"pusher":{"login":"wkolowski","name":"Wojciech Kołowski","path":"/wkolowski","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3518202?s=80&v=4"},"commit":{"message":"Paper: Bidirectional Typing.","shortMessageHtmlLink":"Paper: Bidirectional Typing."}},{"before":"efe6b8409a00cf9be7e3a7914bc9609f284469df","after":"d1b39c6465fd2e450056eb3622e4321fd3e32b54","ref":"refs/heads/master","pushedAt":"2023-12-11T01:03:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"wkolowski","name":"Wojciech Kołowski","path":"/wkolowski","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3518202?s=80&v=4"},"commit":{"message":"Remove the rule Contr : Contr. Reformat some tables related to universes. Write a cautionary paragraph on homotopy levels and predicative levels.","shortMessageHtmlLink":"Remove the rule Contr : Contr. Reformat some tables related to univer…"}},{"before":"289d250649d18b22bdd9971a4a9f83d44c9a7869","after":"efe6b8409a00cf9be7e3a7914bc9609f284469df","ref":"refs/heads/master","pushedAt":"2023-12-10T22:58:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"wkolowski","name":"Wojciech Kołowski","path":"/wkolowski","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3518202?s=80&v=4"},"commit":{"message":"Fix some issues with the Table of Contents.","shortMessageHtmlLink":"Fix some issues with the Table of Contents."}},{"before":"6029600fcea30aaec2ad27394283e85698ae4f27","after":"289d250649d18b22bdd9971a4a9f83d44c9a7869","ref":"refs/heads/master","pushedAt":"2023-12-10T22:49:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"wkolowski","name":"Wojciech Kołowski","path":"/wkolowski","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3518202?s=80&v=4"},"commit":{"message":"Add a warning regarding the Char and Text types. Add a link to new paper on subtype universes.","shortMessageHtmlLink":"Add a warning regarding the Char and Text types. Add a link to new pa…"}},{"before":"c370b98fb3d45318926384a0505e5f666a2e56b8","after":"6029600fcea30aaec2ad27394283e85698ae4f27","ref":"refs/heads/master","pushedAt":"2023-12-09T22:56:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"wkolowski","name":"Wojciech Kołowski","path":"/wkolowski","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3518202?s=80&v=4"},"commit":{"message":"Fix example of subtype universes. Fix description of coercions for primitive integers. Add coercions between primitive integers and primitive floats.","shortMessageHtmlLink":"Fix example of subtype universes. Fix description of coercions for pr…"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEfeXBhgA","startCursor":null,"endCursor":null}},"title":"Activity · wkolowski/Type-Theory-Wishlist"}