{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":17321421,"defaultBranch":"master","name":"UniMath","ownerLogin":"UniMath","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2014-03-01T18:37:12.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/6826454?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1711883599.0","currentOid":""},"activityList":{"items":[{"before":"6f25862d5778b4c9775a6c3ba9ad9fae5dd9427a","after":"0e112eab88b35f7fa3fc83698a87f36e6d1a2b1d","ref":"refs/heads/master","pushedAt":"2024-06-02T11:40:09.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"Basic theory of lax extensions (#1888)\n\nThis PR contains some basic theory of lax extension. \r\n- Definition of lax extensions\r\n- Equivalence of functors with a lax extension and lax double functors","shortMessageHtmlLink":"Basic theory of lax extensions (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2325323362\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1888\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1888/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1888\">#1888</a>)"}},{"before":"419f9aef8d4755227cd801e27df723a0b6095f2a","after":"6f25862d5778b4c9775a6c3ba9ad9fae5dd9427a","ref":"refs/heads/master","pushedAt":"2024-05-27T07:50:04.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"Quantale valued relation and coalgebras (#1887)\n\nThis PR adds two more examples of double categories:\r\n- relations valued in a quantale\r\n- coalgebras for a lax double functor","shortMessageHtmlLink":"Quantale valued relation and coalgebras (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2317855185\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1887\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1887/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1887\">#1887</a>)"}},{"before":"f24ba3ee3bb60ef77e492b2a37be165baccecf7e","after":"419f9aef8d4755227cd801e27df723a0b6095f2a","ref":"refs/heads/master","pushedAt":"2024-05-22T13:44:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"The double bicategory of enriched profunctors (#1886)\n\nThis PR contains:\r\n- The Verity double bicategory of enriched profunctors\r\n- The pseudo double category of profunctors enriched over a quantale\r\n\r\nFor the second point, I also developed some theory of posetal\r\ncategories.","shortMessageHtmlLink":"The double bicategory of enriched profunctors (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2309746615\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1886\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1886/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1886\">#1886</a>)"}},{"before":"95c2c5234e8c2edb5033d8758956f3ecbf18a999","after":"f24ba3ee3bb60ef77e492b2a37be165baccecf7e","ref":"refs/heads/master","pushedAt":"2024-05-21T13:50:31.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"Clean up the Domains and Rings algebra files (#1885)\n\nIncrease the amount of notation used, replace `destruct` by `induction`,\r\nremove redundant brackets. Terms that have been replaced by notation\r\ninclude `paths`, `neg`, `pathsinv0`, `pathscomp0`, `make_dirprod`,\r\n`tpair`, `fun` and `dirprod`.\r\n\r\n---------\r\n\r\nCo-authored-by: Benedikt Ahrens <benedikt.ahrens@gmx.net>","shortMessageHtmlLink":"Clean up the Domains and Rings algebra files (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2304078335\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1885\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1885/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1885\">#1885</a>)"}},{"before":"2b9df86024c21fb6237423cc2c8edcf9c385968f","after":"95c2c5234e8c2edb5033d8758956f3ecbf18a999","ref":"refs/heads/master","pushedAt":"2024-05-19T10:19:06.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"Composition of enriched profunctors (#1882)\n\nThis PR contains:\r\n- definition of enriched profunctors\r\n- unitors and associators\r\n- whiskering operation\r\n\r\nIt also develops the infrastructure necessary for these operations. I\r\nalso fixed a mistake that I made with the notation of enriched\r\nprofunctors (accidentally swapped it around).","shortMessageHtmlLink":"Composition of enriched profunctors (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2278146693\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1882\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1882/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1882\">#1882</a>)"}},{"before":"7432feea2113a460eb5a69fbbba5fda02e2bf234","after":"2b9df86024c21fb6237423cc2c8edcf9c385968f","ref":"refs/heads/master","pushedAt":"2024-05-14T03:29:08.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"Improve notation in BinaryOperations, Groups and Monoids, split Groups and Monoids (#1884)\n\nThis PR changes to the following unicode notations:\r\n  * `∑ _, _` instead of `total2 _ _`\r\n  * `_ = _` instead of `paths _ _`\r\n  * `_ @ _` instead of `pathscomp0 _ _`\r\n  * `!_` instead of `pathsinv0 _ _`\r\n  * `_ × _` instead of `dirprod _ _`\r\n  * `_ ,, _` instead of `make_dirprod _ _` or `tpair _ _ _`\r\n  * `_ → _` instead of `_ -> _`\r\n  * `∃ _, _` instead of `hexists _ _`\r\n  * `λ _, _` instead of `fun _ => _`\r\n  * `1` or `0` instead of `unel _ _` wherever possible\r\n  * `_ * _` or `_ + _` instead of `op _ _ _` wherever possible\r\n  * `x^-1` or `-x` instead of `grinv _ _` wherever possible\r\n \r\nAdditionally, it splits `Groups.v` into `Groups2.v` and\r\n`AbelianGroups.v` (keeping `Groups.v` as a file with two `Require\r\nExport` statements, to not break dependencies), and the same for\r\n`Monoids.v`.","shortMessageHtmlLink":"Improve notation in BinaryOperations, Groups and Monoids, split Group…"}},{"before":"99dc04cbf645ca792526aed39530e67d2ef660f8","after":"7432feea2113a460eb5a69fbbba5fda02e2bf234","ref":"refs/heads/master","pushedAt":"2024-05-04T13:22:14.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rmatthes","name":"Ralph Matthes","path":"/rmatthes","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12064214?s=80&v=4"},"commit":{"message":"multi-sorted binding signatures for untyped and typed forests (#1881)\n\nForests from https://doi.org/10.1016/j.apal.2021.103026 with and without types, as multi-sorted binding signatures, with constructors","shortMessageHtmlLink":"multi-sorted binding signatures for untyped and typed forests (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2278135924\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1881\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1881/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1881\">#1881</a>)"}},{"before":"e4adb3886b064aaf723d0f89412dc862340dc55a","after":"99dc04cbf645ca792526aed39530e67d2ef660f8","ref":"refs/heads/master","pushedAt":"2024-05-01T10:17:53.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"Enriched profunctors (#1880)\n\nThis PR develops the basics of enriched profunctors. The main idea is to\r\nuse a whiskered presentation of profunctors, which is similar to how\r\nmonoidal categories and bicategories are developed. The reason for this\r\nchoice, is that the ultimate definition of profunctor becomes simpler\r\nand more usable. For that purpose, whiskered and curried enriched\r\nbifunctors are developed, and they are shown to be equivalent to the\r\nusual definition.\r\n\r\nOther stuff in this PR are transformations between enriched profunctors\r\n(again in a whiskered style), and some of the main examples of enriched\r\nprofunctors and transformations between them.\r\n\r\n---------\r\n\r\nCo-authored-by: Benedikt Ahrens <benedikt.ahrens@gmail.com>","shortMessageHtmlLink":"Enriched profunctors (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2271186861\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1880\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1880/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1880\">#1880</a>)"}},{"before":"20323781506b92718a1a394959e6c84e2de830f7","after":"e4adb3886b064aaf723d0f89412dc862340dc55a","ref":"refs/heads/master","pushedAt":"2024-04-29T07:18:05.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"adds a forgotten Section around the development with parameter (#1879)\n\nFixes issue #1876.\r\n\r\nCo-authored-by: Ralph Matthes <rmatthes@users.noreply.github.com>","shortMessageHtmlLink":"adds a forgotten Section around the development with parameter (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2268279797\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1879\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1879/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1879\">#1879</a>)"}},{"before":"53dff0a1805e475637eba591ab8d9758cc4b8a70","after":"20323781506b92718a1a394959e6c84e2de830f7","ref":"refs/heads/master","pushedAt":"2024-04-27T12:06:43.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"some beautification of package SubstitutionSystems (#1878)\n\nmostly just cleaning code, but also a mild generalization of results for\n`Id_H` to `Cont_plus_H`, which is currently more a hygiene measure\n\n---------\n\nCo-authored-by: Ralph Matthes <rmatthes@users.noreply.github.com>","shortMessageHtmlLink":"some beautification of package SubstitutionSystems (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2266923261\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1878\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1878/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1878\">#1878</a>)"}},{"before":"499d4223fd766b880299800023ddb43e0bb3a15d","after":"53dff0a1805e475637eba591ab8d9758cc4b8a70","ref":"refs/heads/master","pushedAt":"2024-04-12T11:25:13.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"More examples of double categories (#1875)\n\nThis adds one more example of a double category (coming from\r\ncoreflections) and one of a Verity double bicategory (coming from the\r\nmate calculus).","shortMessageHtmlLink":"More examples of double categories (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2238044956\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1875\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1875/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1875\">#1875</a>)"}},{"before":"9c107c784d9a126071d4237e77e2226d5c1a5a4c","after":"499d4223fd766b880299800023ddb43e0bb3a15d","ref":"refs/heads/master","pushedAt":"2024-04-11T15:43:36.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"Adapt to https://github.com/coq/coq/pull/18880 (#1874)\n\nAdapt to https://github.com/coq/coq/pull/18880\r\n\r\nThis is strictly equivalent but avoids a warning / error.","shortMessageHtmlLink":"Adapt to <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2220462199\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18880\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18880/hovercard\" href=\"https://github.com/coq/coq/pull/18880\">coq/coq#18880</a> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2237697990\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1874\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1874/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1874\">#1874</a>)"}},{"before":"e8b4edb59a9d522d83cffd27255d859ed98dbaef","after":"9c107c784d9a126071d4237e77e2226d5c1a5a4c","ref":"refs/heads/master","pushedAt":"2024-04-10T07:55:54.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"More examples of double categories (#1873)\n\nThis PR contains several examples of double categories.\r\n\r\n---------\r\n\r\nCo-authored-by: Benedikt Ahrens <benedikt.ahrens@gmail.com>","shortMessageHtmlLink":"More examples of double categories (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2234179509\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1873\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1873/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1873\">#1873</a>)"}},{"before":"c8eb2c8506a51f846cf1a1ee1d87e95bc25238ad","after":"e8b4edb59a9d522d83cffd27255d859ed98dbaef","ref":"refs/heads/master","pushedAt":"2024-04-08T19:09:20.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"Clairambault's and Dybjer's theorem for toposes (#1872)\n\nIn this PR, I extend the biequivalence by Clairambault and Dybjer to\r\nseveral classes of toposes to give internal languages of toposes. The PR\r\nalso contains a development of locally Cartesian closed categories.\r\n\r\n---------\r\n\r\nCo-authored-by: Ralph Matthes <ralph.matthes@irit.fr>\r\nCo-authored-by: Benedikt Ahrens <benedikt.ahrens@gmail.com>","shortMessageHtmlLink":"Clairambault's and Dybjer's theorem for toposes (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2222350043\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1872\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1872/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1872\">#1872</a>)"}},{"before":"0aabc23943c828d7e7952ae5f23f11586e7e39ea","after":"c8eb2c8506a51f846cf1a1ee1d87e95bc25238ad","ref":"refs/heads/master","pushedAt":"2024-04-03T06:59:05.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"Clairambault&Dybjer's biequivalence for regular/exact categories and pretoposes (#1870)\n\nThis PR contains:\r\n- Formalization of regular and of exact categories\r\n- A proof that being regular and being exact are local properties\r\n- The product of displayed biequivalences\r\n\r\nFrom the second point of these, we can extend the biequivalence by\r\nClairambault and Dybjer to regular/exact categories. As a consequence,\r\nwe can also extend it to pretoposes.\r\n\r\n---------\r\n\r\nCo-authored-by: Ralph Matthes <ralph.matthes@irit.fr>\r\nCo-authored-by: Benedikt Ahrens <benedikt.ahrens@gmail.com>\r\nCo-authored-by: Benedikt Ahrens <benedikt.ahrens@gmx.net>","shortMessageHtmlLink":"Clairambault&amp;Dybjer's biequivalence for regular/exact categories and …"}},{"before":"105485682825cc807aed812fe13a44363f81f372","after":"0aabc23943c828d7e7952ae5f23f11586e7e39ea","ref":"refs/heads/master","pushedAt":"2024-04-02T17:58:31.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rmatthes","name":"Ralph Matthes","path":"/rmatthes","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12064214?s=80&v=4"},"commit":{"message":"avoids one kind of warning when compiling UniMath (#1871)\n\nonly one occurrence, but right in the beginning, which might be\r\nirritating\r\n\r\nCo-authored-by: Ralph Matthes <rmatthes@users.noreply.github.com>","shortMessageHtmlLink":"avoids one kind of warning when compiling UniMath (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2220911312\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1871\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1871/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1871\">#1871</a>)"}},{"before":"b4d5ea5fe8d8f423b9c48fae4b478e86f6595f49","after":"105485682825cc807aed812fe13a44363f81f372","ref":"refs/heads/master","pushedAt":"2024-03-31T09:58:28.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rmatthes","name":"Ralph Matthes","path":"/rmatthes","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12064214?s=80&v=4"},"commit":{"message":"the STLC example in the actegorical setting, with Church numerals (#1869)\n\nsimply-typed lambda calculus represented through a multi-sorted binding\r\nsignature, with inductive and with coinductive interpretation, over base\r\ncategory HSET (this continues the rudimentary example presentation in PR\r\n#1844 in addressing and establishing naturality) and over an abstract\r\ncategory\r\n\r\nconstruction of the typed Church numerals, including the Church numeral\r\nfor infinity in the coinductive interpretation (with its characteristic\r\nfixed-point equation)\r\n\r\n---------\r\n\r\nCo-authored-by: Ralph Matthes <rmatthes@users.noreply.github.com>","shortMessageHtmlLink":"the STLC example in the actegorical setting, with Church numerals (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2206243588\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1869\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1869/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1869\">#1869</a>"}},{"before":"b434ef278156e6ba5777b15dd55716fb8bedd8ef","after":"b4d5ea5fe8d8f423b9c48fae4b478e86f6595f49","ref":"refs/heads/master","pushedAt":"2024-03-26T09:25:53.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"Another extension the biequivalence by Clairambault and Dybjer (#1866)\n\nThis PR contains the following:\r\n- More development of subobject classifiers (the slice category has\r\nsubobject classifiers, preservation of subobject classifiers)\r\n- A couple of minor refactorings\r\n- An extension of the biequivalence by Clairambault and Dybjer to\r\nsubobject classifier types\r\n\r\nNote: I do not use local properties for subobject classifiers (which was\r\nthe topic of the previous PR), and an explanation is in the\r\ndocumentation. The next extension will be for regular/exact categories\r\n(i.e., quotient types).\r\n\r\n---------\r\n\r\nCo-authored-by: Benedikt Ahrens <benedikt.ahrens@gmail.com>","shortMessageHtmlLink":"Another extension the biequivalence by Clairambault and Dybjer (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2203357495\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1866\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1866/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1866\">#1866</a>)"}},{"before":"e56206616f4799d52a7307bc8abbd766d3340afa","after":"b434ef278156e6ba5777b15dd55716fb8bedd8ef","ref":"refs/heads/master","pushedAt":"2024-03-25T15:29:14.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"Document a file (#1868)\n\nI forgot to document a file, and now the comments are added.","shortMessageHtmlLink":"Document a file (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2205211962\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1868\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1868/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1868\">#1868</a>)"}},{"before":"4b856a703b1cba32059d8cd7eebf3c2d43040fcf","after":"e56206616f4799d52a7307bc8abbd766d3340afa","ref":"refs/heads/master","pushedAt":"2024-03-24T19:02:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"Improve some names (#1867)\n\n- `horizontal_setbicat` is renamed to `horizontal_bisetcat`\r\n- Add an identifier for when a double category is univalent and use that\r\none\r\n- `strict_profunctor_univalent_double_cat` is renamed to\r\n`setcat_profunctor_univalent_double_cat`\r\n- `univalent_profunctor_verity_double_bicat` is renamed to\r\n`univcat_profunctor_verity_double_bicat`","shortMessageHtmlLink":"Improve some names (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2204305762\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1867\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1867/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1867\">#1867</a>)"}},{"before":"8f45384489c9af642dfe395f6aa43a5438ae1cf7","after":"4b856a703b1cba32059d8cd7eebf3c2d43040fcf","ref":"refs/heads/master","pushedAt":"2024-03-22T21:28:59.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"Update bibliography with the latest tag (#1865)","shortMessageHtmlLink":"Update bibliography with the latest tag (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2200267238\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1865\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1865/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1865\">#1865</a>)"}},{"before":"0efbb744f63d703143a81b62c6ad04ba6b0dd71f","after":"8f45384489c9af642dfe395f6aa43a5438ae1cf7","ref":"refs/heads/master","pushedAt":"2024-03-21T13:57:34.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"restores dev build of satellite GrpdHITs in GitHub CI (#1864)\n\nsome comments updated\r\n\r\nCo-authored-by: Ralph Matthes <rmatthes@users.noreply.github.com>","shortMessageHtmlLink":"restores dev build of satellite GrpdHITs in GitHub CI (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2197871410\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1864\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1864/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1864\">#1864</a>)"}},{"before":"1a710b32e4a9330f446fe215b1dab6ab861e7d9c","after":"0efbb744f63d703143a81b62c6ad04ba6b0dd71f","ref":"refs/heads/master","pushedAt":"2024-03-18T14:37:46.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"Extending the biequivalence by Clairambault and Dybjer to local properties (#1862)\n\nThis PR contains an extension of the biequivalence by Clairambault and\r\nDybjer to include local properties of categories. Currently, the example\r\nof this is given by lextensive categories, so we get a biequivalence\r\nbetween the bicategory of univalent lextensive categories and democratic\r\nfull comprehension categories with ∑, extensional identity, empty types,\r\nand sum types.","shortMessageHtmlLink":"Extending the biequivalence by Clairambault and Dybjer to local prope…"}},{"before":"63aa4d14e8683a3608f94896d50f4f1a0a3fb3ac","after":"1a710b32e4a9330f446fe215b1dab6ab861e7d9c","ref":"refs/heads/master","pushedAt":"2024-03-11T11:39:29.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rmatthes","name":"Ralph Matthes","path":"/rmatthes","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12064214?s=80&v=4"},"commit":{"message":"general definition of global elements (#1861)\n\nslight modification of names for better harmony\r\nglobal elements in functor categories\r\n\r\n---------\r\n\r\nCo-authored-by: Ralph Matthes <rmatthes@users.noreply.github.com>","shortMessageHtmlLink":"general definition of global elements (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2178725006\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1861\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1861/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1861\">#1861</a>)"}},{"before":"6d15bef67b1b094fabebff70557a5aa51add4861","after":"63aa4d14e8683a3608f94896d50f4f1a0a3fb3ac","ref":"refs/heads/master","pushedAt":"2024-03-08T14:55:20.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"rmatthes","name":"Ralph Matthes","path":"/rmatthes","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12064214?s=80&v=4"},"commit":{"message":"reduce number of reversible coercions (#1859)\n\nThis partially undoes PR #1850.\r\n\r\nCurrently, it concerns 99 of the 259 reversibility declarations. I only\r\nfound 5 worthy to retain. I'll try to look at the others as well.\r\n\r\nUnfortunately, this PR sits on the already merged PR #1858. So, only my\r\ncommits are relevant. The file comparison should be okay (not be\r\ncluttered because of that).\r\n\r\nUpdate: 250 of the 259 reversibility declarations are now gone. In one\r\nsingle case was the need for reversibility circumvented by a small code\r\nmodification. The other 9 reversible coercions are now in use. If CI\r\ngoes well, this completes the present PR.","shortMessageHtmlLink":"reduce number of reversible coercions (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2172228368\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1859\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1859/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1859\">#1859</a>)"}},{"before":"6605a4a22a7dcda5d27025b9c75ae2f905338b6f","after":"6d15bef67b1b094fabebff70557a5aa51add4861","ref":"refs/heads/master","pushedAt":"2024-03-06T19:43:23.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"The biequivalence by Clairambault and Dybjer (#1857)\n\nThis PR contains one of the biequivalences by Clairambault and Dybjer.\r\nMore specifically, I construct a biequivalence between the bicategory of\r\nunivalent categories with finite limits and univalent comprehension\r\ncategories that are democratic and with some type formers\r\n(`finlim_biequiv_dfl_comp_cat_psfunctor` in the file `Biequiv`). There\r\nis also some stuff about adjoint equivalences of comprehension\r\ncategories. Here univalence is used, because it contains multiple usages\r\nof induction on equivalences.","shortMessageHtmlLink":"The biequivalence by Clairambault and Dybjer (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2169643350\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1857\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1857/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1857\">#1857</a>)"}},{"before":"abe1a92c3f7c800ba4aafa72cbec70bb70d16f97","after":"6605a4a22a7dcda5d27025b9c75ae2f905338b6f","ref":"refs/heads/master","pushedAt":"2024-03-06T17:08:19.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"Optimizing Model Categories (#1858)\n\nFor fixing #1855 \r\n\r\nI have yet to test how long it takes to `make ModelCategories` from\r\nscratch on my 8 year old laptop through WSL, but I believe it is within\r\na reasonable time on my 8 year old laptop with:\r\n- i5 7200U quad core @ 2.5GHz\r\n- 8GB 2133MHz memory\r\nI hope the CLI is faster than this extremely bottlenecked setup, but who\r\nknows...\r\n\r\nThe LNWFSMonoidalStructure (~5min), LNWFSCocomplete.v, LNWFSClosed.v and\r\nLNWFSSmallnessReduction.v files\r\nstill seem to take the longest, but this should be enough to compile\r\nwithin the time limit I would think.\r\nIt kind of dazzles me though, since on Windows, and with a slightly\r\nolder version of UniMath, and Coq 8.17\r\nthe LNWFSClosed and LNWFSSmallnessReduction files take up literally half\r\na minute. What makes these\r\nfiles different is that there are two proofs where I try to show an\r\nLNWFS structure `L -->[mor] L'` on `mor`,\r\ngiven an LNWFS structure `L -->[mor'] L'` for `mor' = mor`, so to say. I\r\nused to use a rewrite in the proof,\r\nwhich seems to cause the slowness. Now I abstracted that to an opaque\r\nproof, which seems to speed up the\r\nprocess slightly, but it is still pretty slow... \r\n\r\nI am not sure if there is already a CLI check for the ModelCategories\r\npackage, but I would like to know if the\r\nfiles compile properly in the GitHub CLI as well. Preferably this should\r\nhappen kind of soon, since I am in the\r\nprocess of writing an article on this theory based on my thesis,\r\nsupervised by Paige North, and it would be very\r\nvaluable if the theory is (properly) integrated into the UniMath\r\nlibrary.\r\n\r\nStrategies for improving the compile times include sectioning and adding\r\nContext variables, splitting up some proofs, making certain terms Opaque\r\nwithin the file and shortening some proofs. I will work on it a bit more\r\ntomorrow and get back to it in this PR.","shortMessageHtmlLink":"Optimizing Model Categories (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2170222235\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1858\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1858/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1858\">#1858</a>)"}},{"before":"733e837f13aac6a11ea1e7a6c42ada2990964db9","after":"abe1a92c3f7c800ba4aafa72cbec70bb70d16f97","ref":"refs/heads/master","pushedAt":"2024-03-01T15:12:02.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"more consequent use of the sum of a constant functor and the domain-s… (#1844)\n\n…pecific functor\r\n\r\nThis is for the construction of the variable inclusion and the other\r\nconstructors.\r\n\r\nSubstitutionSystems.v: Id_H generalized to Const_plus_H, Id_H is then an\r\ninstance\r\nthe constructors eta and tau are now for the more general situation\r\nLiftingInitial_alt.v only instantiates these notions from\r\nSubstitutionSystems.v LiftingInitial.v: idem\r\nMonadsFromSubstitutionSystems.v: def. of Id_H deleted STLC.v now refers\r\nto SubstitutionSystems.v for Id_H and uses eta for var_map STLC_alt.v\r\nuses eta for var_map\r\nMLTT79.v now refers to SubstitutionSystems.v for Id_H SimplifiedHSS gets\r\nthe same changes\r\n\r\nMultiSortedMonadConstruction_(coind_)actegorical.v now refers to\r\nSubstitutionSystems.v for Id_H\r\n\r\nLam.v exactly uses eta and tau (the latter for the pseudo-constructor\r\nLam_App_Abs) the development now gets help with type information and\r\nthere is a certain reorganization of the proof of\r\nbracket_for_LamE_algebra_on_Lam_unique SimplifiedHSS/Lam.v is similar\r\nbut does not have the statement bracket_for_LamE_algebra_on_Lam_unique","shortMessageHtmlLink":"more consequent use of the sum of a constant functor and the domain-s… ("}},{"before":"a025e583854a0bee42b790d283ea1bed698c5341","after":"733e837f13aac6a11ea1e7a6c42ada2990964db9","ref":"refs/heads/master","pushedAt":"2024-02-29T22:50:30.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"benediktahrens","name":"Benedikt Ahrens","path":"/benediktahrens","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1106102?s=80&v=4"},"commit":{"message":"restore compilation with Coq 8.20 dev version (#1856)\n\nThis has the same objective as PR #1848 and deals with a future problem\r\nof code that was merged in the meantime.","shortMessageHtmlLink":"restore compilation with Coq 8.20 dev version (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2161865672\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1856\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1856/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1856\">#1856</a>)"}},{"before":"0c15d0891168d72a9853d6a23b5d974bbdf0f2aa","after":"a025e583854a0bee42b790d283ea1bed698c5341","ref":"refs/heads/master","pushedAt":"2024-02-28T11:49:07.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"nmvdw","name":"Niels van der Weide","path":"/nmvdw","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24875025?s=80&v=4"},"commit":{"message":"Adapt to https://github.com/coq/coq/pull/18705 (#1850)\n\nAdapt to https://github.com/coq/coq/pull/18705\r\nThis is backward compatible (down to Coq 8.16).\r\n\r\nCo-authored-by: Niels van der Weide <nnmvdw@gmail.com>","shortMessageHtmlLink":"Adapt to <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2148789485\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18705\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18705/hovercard\" href=\"https://github.com/coq/coq/pull/18705\">coq/coq#18705</a> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2152511476\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1850\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1850/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1850\">#1850</a>)"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEWiTwBAA","startCursor":null,"endCursor":null}},"title":"Activity · UniMath/UniMath"}