{"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":"2d7044008cb9a2faa8d1c1c6b926ada9ac278f8d","after":"5dd6800a2c8567b4bf80efa3389d6d16015861d5","ref":"refs/heads/master","pushedAt":"2024-06-27T13:39:18.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":"Univalence statements for double bicats (#1897)\n\nThis PR adds some summarizing statements for univalent double\r\nbicategories","shortMessageHtmlLink":"Univalence statements for double bicats (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2375089299\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1897\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1897/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1897\">#1897</a>)"}},{"before":"179b179cc7a55118f2319335fc75a16e35b0dc1d","after":"2d7044008cb9a2faa8d1c1c6b926ada9ac278f8d","ref":"refs/heads/master","pushedAt":"2024-06-24T15:23:49.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":" Show that under some circumstances, two precomposition functors that together are an adjoint equivalence, are also themselves adjoint equivalences (#1895)","shortMessageHtmlLink":" Show that under some circumstances, two precomposition functors that…"}},{"before":"05b0156b527423f980c493317a766d665b5e1401","after":"179b179cc7a55118f2319335fc75a16e35b0dc1d","ref":"refs/heads/master","pushedAt":"2024-06-22T08:36:05.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 theory of extensions (#1891)\n\nFormalize the theory algebras `T_n`, algebra pullbacks `F* A` and the\r\ntheory of extensions `T_A` as a functor from `T`-algebras to algebraic\r\ntheories. Show that the category of `T_A`-algebras is equivalent to the\r\ncoslice category under `A`, and show that any algebraic theory morphism\r\n`F : S -> T` factors through `S_{F* T_0}`.","shortMessageHtmlLink":"The theory of extensions (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2346259145\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1891\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1891/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1891\">#1891</a>)"}},{"before":"d702c868514047936ee4e71451d8db515295b9fd","after":"05b0156b527423f980c493317a766d665b5e1401","ref":"refs/heads/master","pushedAt":"2024-06-14T13:01: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":"Some more theory of double categories (#1889)\n\nThis PR also contains #1888 . The additional content is:\r\n- flat double categories and examples\r\n- double terminal objects\r\n- graphs and collages of enriched profunctors\r\n\r\n---------\r\n\r\nCo-authored-by: Benedikt Ahrens <benedikt.ahrens@gmx.net>","shortMessageHtmlLink":"Some more theory of double categories (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2329248954\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1889\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1889/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1889\">#1889</a>)"}},{"before":"8becb1d0881abc6117fdf403559d38c92b501ded","after":"d702c868514047936ee4e71451d8db515295b9fd","ref":"refs/heads/master","pushedAt":"2024-06-13T16:50: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":"remove check (#1894)","shortMessageHtmlLink":"remove check (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2351047549\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1894\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1894/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1894\">#1894</a>)"}},{"before":"cd7f912c744d6d3ff944fcfd2963dd2dcee579e4","after":"8becb1d0881abc6117fdf403559d38c92b501ded","ref":"refs/heads/master","pushedAt":"2024-06-12T11:06: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":"Reasoning with foldr1_map (#1893)\n\nThe idea is to have a lemma as interface instead of going into the\r\ndetails of the encoding of lists.\r\n\r\nThis is shown to be useful for non-trivial situations in package\r\nSubstitutionSystems.","shortMessageHtmlLink":"Reasoning with foldr1_map (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2346806849\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1893\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1893/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1893\">#1893</a>)"}},{"before":"0e112eab88b35f7fa3fc83698a87f36e6d1a2b1d","after":"cd7f912c744d6d3ff944fcfd2963dd2dcee579e4","ref":"refs/heads/master","pushedAt":"2024-06-10T08:21:25.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":"Original representation theorem (#1890)\n\n* Partially add Scott's original (1980) proof of his representation\r\ntheorem;\r\n* Define a tactic (in `Combinators`) to help generate `refine`\r\nstatements for proving equality between lambda terms;\r\n* To make this work, re-add some definitions (like `subst_subst_ax`) to\r\nthe object files (as opposed to the category files), because the old\r\napproach broke the tactic (generating terms like `pr121 T f g` instead\r\nof `subst f g`);\r\n* Using these two, rewrite parts of the \"algebra to theory\" file,\r\ndeprecating `LambdaTerms.v`;\r\n* Rename `pr` to `var` and `comp` to `subst`, to be more consistent with\r\nthe lambda calculus view.","shortMessageHtmlLink":"Original representation theorem (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2333735169\" data-permission-text=\"Title is private\" data-url=\"https://github.com/UniMath/UniMath/issues/1890\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/UniMath/UniMath/pull/1890/hovercard\" href=\"https://github.com/UniMath/UniMath/pull/1890\">#1890</a>)"}},{"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…"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEcOFF-QA","startCursor":null,"endCursor":null}},"title":"Activity · UniMath/UniMath"}