{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":15994976,"defaultBranch":"master","name":"agda-stdlib","ownerLogin":"agda","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2014-01-17T09:09:18.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/410000?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1717767304.0","currentOid":""},"activityList":{"items":[{"before":"aeb212c5e7ffd3386c12084ef2d6828ba7ddd55b","after":"522053d94c73375e6a5f6f075f86df25e706e64e","ref":"refs/heads/PremoveDecToMaybe","pushedAt":"2024-06-09T08:30:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jamesmckinna","name":null,"path":"/jamesmckinna","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/31931406?s=80&v=4"},"commit":{"message":"fix `CHANGELOG`","shortMessageHtmlLink":"fix <code>CHANGELOG</code>"}},{"before":"710b25a030e30cf7eaac296b6564be536df51917","after":"aeb212c5e7ffd3386c12084ef2d6828ba7ddd55b","ref":"refs/heads/PremoveDecToMaybe","pushedAt":"2024-06-09T08:26:24.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"jamesmckinna","name":null,"path":"/jamesmckinna","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/31931406?s=80&v=4"},"commit":{"message":"deprecation via delegation","shortMessageHtmlLink":"deprecation via delegation"}},{"before":"9445cdfcb782909dc02d6542ada5fd0220b35163","after":"0e8b7577c1f5e433f9aab1896c998d0842f07f50","ref":"refs/heads/gh-pages","pushedAt":"2024-06-07T14:46:14.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/agda-stdlib@ad0fb0efc58b03bf9ebc83eba6ae513c3aa7a073 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/agda-stdlib/commit/ad0fb0efc58b03bf9ebc83eba6ae513c3aa7a073/hovercard\" href=\"https://github.com/agda/agda-stdlib/commit/ad0fb0efc58b03bf9ebc83eba6ae513c3aa7a073\"><tt>ad0fb0e</tt></a> 🚀"}},{"before":"ad0fb0efc58b03bf9ebc83eba6ae513c3aa7a073","after":null,"ref":"refs/heads/gh-readonly-queue/master/pr-2402-08f24a61a418c0f29d11588ffa921566c4e50d9e","pushedAt":"2024-06-07T14:10:19.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"}},{"before":"08f24a61a418c0f29d11588ffa921566c4e50d9e","after":"ad0fb0efc58b03bf9ebc83eba6ae513c3aa7a073","ref":"refs/heads/master","pushedAt":"2024-06-07T14:10:18.000Z","pushType":"merge_queue_merge","commitsCount":1,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"Add `IsIdempotentMonoid` and `IsCommutativeBand` to `Algebra.Structures` (#2402)\n\n* fix #2138\n\n* fixed `Structures`; added `Bundles`\n\n* added fields; plus redefined `IsSemilattice` and `IsBoundedSemilattice` as aliases\n\n* `fix-whitespace`\n\n* reexported `comm`\n\n* fixed `Lattice.Bundles`\n\n* knock-on\n\n* added text about redefinition of `Is(Bounded)Semilattice`\n\n* add manifest fields to `IsIdempotentSemiring`\n\n* final missing `Bundles`\n\n* `CHANGELOG`","shortMessageHtmlLink":"Add <code>IsIdempotentMonoid</code> and <code>IsCommutativeBand</code> to `Algebra.Structur…"}},{"before":null,"after":"ad0fb0efc58b03bf9ebc83eba6ae513c3aa7a073","ref":"refs/heads/gh-readonly-queue/master/pr-2402-08f24a61a418c0f29d11588ffa921566c4e50d9e","pushedAt":"2024-06-07T13:35:04.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"Add `IsIdempotentMonoid` and `IsCommutativeBand` to `Algebra.Structures` (#2402)\n\n* fix #2138\n\n* fixed `Structures`; added `Bundles`\n\n* added fields; plus redefined `IsSemilattice` and `IsBoundedSemilattice` as aliases\n\n* `fix-whitespace`\n\n* reexported `comm`\n\n* fixed `Lattice.Bundles`\n\n* knock-on\n\n* added text about redefinition of `Is(Bounded)Semilattice`\n\n* add manifest fields to `IsIdempotentSemiring`\n\n* final missing `Bundles`\n\n* `CHANGELOG`","shortMessageHtmlLink":"Add <code>IsIdempotentMonoid</code> and <code>IsCommutativeBand</code> to `Algebra.Structur…"}},{"before":"c25df84534e4363cb439ea4d6d964c582f26436b","after":"9445cdfcb782909dc02d6542ada5fd0220b35163","ref":"refs/heads/gh-pages","pushedAt":"2024-06-07T12:24:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/agda-stdlib@08f24a61a418c0f29d11588ffa921566c4e50d9e 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/agda-stdlib/commit/08f24a61a418c0f29d11588ffa921566c4e50d9e/hovercard\" href=\"https://github.com/agda/agda-stdlib/commit/08f24a61a418c0f29d11588ffa921566c4e50d9e\"><tt>08f24a6</tt></a> 🚀"}},{"before":"08f24a61a418c0f29d11588ffa921566c4e50d9e","after":null,"ref":"refs/heads/gh-readonly-queue/master/pr-2342-c0fafe970d46f64ebd755a854c7c91b41fd2993f","pushedAt":"2024-06-07T11:49:49.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"}},{"before":"c0fafe970d46f64ebd755a854c7c91b41fd2993f","after":"08f24a61a418c0f29d11588ffa921566c4e50d9e","ref":"refs/heads/master","pushedAt":"2024-06-07T11:49:48.000Z","pushType":"merge_queue_merge","commitsCount":1,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"Port two Endomorphism submodules over to new Function hierarchy (#2342)\n\n* port over two modules\n\n* and add to CHANGELOG\n\n* fix whitespace\n\n* fix warning: it was pointing to a record that did not exist.\n\n* fix things as per Matthew's review - though this remains a breaking change.\n\n* take care of comments from James.\n\n* adjust CHANGELOG for what will be implemented shortly\n\n* Revert \"take care of comments from James.\"\n\nThis reverts commit 93e9e0fdf482164c0fb7e709ef8799fbc3fa0385.\n\n* Revert \"fix things as per Matthew's review - though this remains a breaking change.\"\n\nThis reverts commit d1cae72dcb3b44d4ba3c7290f3535544be32ab1e.\n\n* Revert \"fix whitespace\"\n\nThis reverts commit 81230ecf0c8ff634433c9d17d53c9d2e8b3c1fd2.\n\n* Revert \"port over two modules\"\n\nThis reverts commit 6619f114346e86ead3cf62b1170ab23d31056b48.\n\n* rename these\n\n* fix tiny merge issue\n\n* get deprecations right (remove where not needed, make more global where needed)\n\n* style guide - missing blank lines\n\n* fix a bad merge\n\n* fixed deprecations\n\n* fix #2394\n\n* minor tweaks\n\n---------\n\nCo-authored-by: James McKinna <J.McKinna@hw.ac.uk>","shortMessageHtmlLink":"Port two Endomorphism submodules over to new Function hierarchy (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2221719252\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/agda-stdlib/issues/2342\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/agda-stdlib/pull/2342/hovercard\" href=\"https://github.com/agda/agda-stdlib/pull/2342\">#2342</a>)"}},{"before":null,"after":"08f24a61a418c0f29d11588ffa921566c4e50d9e","ref":"refs/heads/gh-readonly-queue/master/pr-2342-c0fafe970d46f64ebd755a854c7c91b41fd2993f","pushedAt":"2024-06-07T11:14:29.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"Port two Endomorphism submodules over to new Function hierarchy (#2342)\n\n* port over two modules\n\n* and add to CHANGELOG\n\n* fix whitespace\n\n* fix warning: it was pointing to a record that did not exist.\n\n* fix things as per Matthew's review - though this remains a breaking change.\n\n* take care of comments from James.\n\n* adjust CHANGELOG for what will be implemented shortly\n\n* Revert \"take care of comments from James.\"\n\nThis reverts commit 93e9e0fdf482164c0fb7e709ef8799fbc3fa0385.\n\n* Revert \"fix things as per Matthew's review - though this remains a breaking change.\"\n\nThis reverts commit d1cae72dcb3b44d4ba3c7290f3535544be32ab1e.\n\n* Revert \"fix whitespace\"\n\nThis reverts commit 81230ecf0c8ff634433c9d17d53c9d2e8b3c1fd2.\n\n* Revert \"port over two modules\"\n\nThis reverts commit 6619f114346e86ead3cf62b1170ab23d31056b48.\n\n* rename these\n\n* fix tiny merge issue\n\n* get deprecations right (remove where not needed, make more global where needed)\n\n* style guide - missing blank lines\n\n* fix a bad merge\n\n* fixed deprecations\n\n* fix #2394\n\n* minor tweaks\n\n---------\n\nCo-authored-by: James McKinna <J.McKinna@hw.ac.uk>","shortMessageHtmlLink":"Port two Endomorphism submodules over to new Function hierarchy (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2221719252\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/agda-stdlib/issues/2342\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/agda-stdlib/pull/2342/hovercard\" href=\"https://github.com/agda/agda-stdlib/pull/2342\">#2342</a>)"}},{"before":"13160dc539307ddd278d176abb798cbbab0943e0","after":"710b25a030e30cf7eaac296b6564be536df51917","ref":"refs/heads/PremoveDecToMaybe","pushedAt":"2024-06-07T02:51:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JacquesCarette","name":"Jacques Carette","path":"/JacquesCarette","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1855141?s=80&v=4"},"commit":{"message":"instead of an alias, open public so that Agda knows these really are the same. This is a better deprecation strategy.","shortMessageHtmlLink":"instead of an alias, open public so that Agda knows these really are …"}},{"before":"278547ab5f3a36bbf2bbd114fc18f30187eab77c","after":"c71cb837bc8bf6e6daca697c662867aebd883f68","ref":"refs/heads/Endomorphism","pushedAt":"2024-06-07T02:07:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"JacquesCarette","name":"Jacques Carette","path":"/JacquesCarette","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1855141?s=80&v=4"},"commit":{"message":"minor tweaks","shortMessageHtmlLink":"minor tweaks"}},{"before":"7a2b429be79d574be6f16bc98869d440d05fdda4","after":"13160dc539307ddd278d176abb798cbbab0943e0","ref":"refs/heads/PremoveDecToMaybe","pushedAt":"2024-06-06T14:36:09.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"jamesmckinna","name":null,"path":"/jamesmckinna","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/31931406?s=80&v=4"},"commit":{"message":"tidy up","shortMessageHtmlLink":"tidy up"}},{"before":"4428f966334bdd496f0e39f29f5fd5c568de1370","after":"7a2b429be79d574be6f16bc98869d440d05fdda4","ref":"refs/heads/PremoveDecToMaybe","pushedAt":"2024-06-06T14:06:49.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"jamesmckinna","name":null,"path":"/jamesmckinna","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/31931406?s=80&v=4"},"commit":{"message":"simplify `import`s","shortMessageHtmlLink":"simplify <code>import</code>s"}},{"before":"256a50589dacab913c69f4db5b4570b46cf440d7","after":"4428f966334bdd496f0e39f29f5fd5c568de1370","ref":"refs/heads/PremoveDecToMaybe","pushedAt":"2024-06-06T13:47:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jamesmckinna","name":null,"path":"/jamesmckinna","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/31931406?s=80&v=4"},"commit":{"message":"Revert \"chnage to `public` re-export of `Relation.Nullary.Decidable.Core.decToMaybe`\"\n\nThis reverts commit 256a50589dacab913c69f4db5b4570b46cf440d7.","shortMessageHtmlLink":"Revert \"chnage to <code>public</code> re-export of `Relation.Nullary.Decidable.C…"}},{"before":"ab16308964bb3ee82a55f9b46995eb7bb45eb5f4","after":"256a50589dacab913c69f4db5b4570b46cf440d7","ref":"refs/heads/PremoveDecToMaybe","pushedAt":"2024-06-06T08:15:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jamesmckinna","name":null,"path":"/jamesmckinna","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/31931406?s=80&v=4"},"commit":{"message":"chnage to `public` re-export of `Relation.Nullary.Decidable.Core.decToMaybe`","shortMessageHtmlLink":"chnage to <code>public</code> re-export of `Relation.Nullary.Decidable.Core.decT…"}},{"before":"7712d985e83fb7f16a17acf01ac7382521540148","after":"ab16308964bb3ee82a55f9b46995eb7bb45eb5f4","ref":"refs/heads/PremoveDecToMaybe","pushedAt":"2024-06-06T08:01:21.000Z","pushType":"push","commitsCount":20,"pusher":{"login":"jamesmckinna","name":null,"path":"/jamesmckinna","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/31931406?s=80&v=4"},"commit":{"message":"Merge branch 'master' into PremoveDecToMaybe","shortMessageHtmlLink":"Merge branch 'master' into PremoveDecToMaybe"}},{"before":"0070b748ef23c3b3ac380b76520f7a00974cd4fa","after":"c25df84534e4363cb439ea4d6d964c582f26436b","ref":"refs/heads/gh-pages","pushedAt":"2024-06-05T16:57:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/agda-stdlib@c0fafe970d46f64ebd755a854c7c91b41fd2993f 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/agda-stdlib/commit/c0fafe970d46f64ebd755a854c7c91b41fd2993f/hovercard\" href=\"https://github.com/agda/agda-stdlib/commit/c0fafe970d46f64ebd755a854c7c91b41fd2993f\"><tt>c0fafe9</tt></a> 🚀"}},{"before":"2857149def8e6b1273d0259d394e28a2ad57300b","after":"0070b748ef23c3b3ac380b76520f7a00974cd4fa","ref":"refs/heads/gh-pages","pushedAt":"2024-06-05T16:40:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/agda-stdlib@b13a032851a99c0abd9ebc55748ad0cbd1e0060d 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/agda-stdlib/commit/b13a032851a99c0abd9ebc55748ad0cbd1e0060d/hovercard\" href=\"https://github.com/agda/agda-stdlib/commit/b13a032851a99c0abd9ebc55748ad0cbd1e0060d\"><tt>b13a032</tt></a> 🚀"}},{"before":"c0fafe970d46f64ebd755a854c7c91b41fd2993f","after":null,"ref":"refs/heads/gh-readonly-queue/master/pr-2324-b13a032851a99c0abd9ebc55748ad0cbd1e0060d","pushedAt":"2024-06-05T16:22:29.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"}},{"before":"b13a032851a99c0abd9ebc55748ad0cbd1e0060d","after":"c0fafe970d46f64ebd755a854c7c91b41fd2993f","ref":"refs/heads/master","pushedAt":"2024-06-05T16:22:27.000Z","pushType":"merge_queue_merge","commitsCount":1,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"Refactor `List.Membership.*` and `List.Relation.Unary.Any` (#2324)\n\n* `contradiction` against `⊥-elim`\n\n* tightened `import`s\n\n* added two operations `∃∈` and `∀∈`\n\n* added to `CHANGELOG`\n\n* knock-on for the `Propositional` case\n\n* refactor `lose∘find` and `find∘lose` in terms of new lemmas `∃∈-Any∘find` and `find∘∃∈-Any`\n\n* `CHANGELOG`\n\n* reorder\n\n* knock-on viscosity\n\n* knock-on viscosity; plus refactoring of `×↔` for intelligibility\n\n* knock-on viscosity\n\n* tightened `import`s\n\n* misc. import and other tweaks\n\n* misc. import and other tweaks\n\n* misc. import and other tweaks\n\n* removed spurious module name\n\n* better definition of `find`\n\n* make intermediate terms explicit in proof of `to∘from`\n\n* tweaks\n\n* Update Setoid.agda\n\nRemove redundant import of `index` from `Any`\n\n* Update Setoid.agda\n\nRemoved more redundant `import`ed operations\n\n* Update Properties.agda\n\nAnother redundant `import`\n\n* Update Properties.agda\n\nAnother redundant `import`ed operation\n\n* `with` into `let`\n\n* `with` into `let`\n\n* `with` into `let`\n\n* `with` into `let`\n\n* indentation\n\n* fix `universal-U`\n\n* added `map-cong`\n\n* deprecate `map-compose` in favour of `map-∘`\n\n* explicit `let` in statement of `find∘map`\n\n* knock-on viscosity: hide `map-cong`\n\n* use of `Product.map₁`\n\n* revert use of `Product.map₁`\n\n* inlined lemmas!\n\n* alpha conversion and further inlining!\n\n* correctted use of `Product.map₂`\n\n* added `syntax` declarations for the new combinators\n\n* remove`⊥-elim`\n\n* reordered `CHANGELOG`\n\n* revise combinator names\n\n* tighten `import`s\n\n* tighten `import`s\n\n* fixed merge conflict bug\n\n* removed new syntax\n\n* knock-on","shortMessageHtmlLink":"Refactor <code>List.Membership.*</code> and <code>List.Relation.Unary.Any</code> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2200010236\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/agda-stdlib/issues/2324\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/agda-stdlib/pull/2324/hovercard\" href=\"https://github.com/agda/agda-stdlib/pull/2324\">#2324</a>)"}},{"before":"b13a032851a99c0abd9ebc55748ad0cbd1e0060d","after":null,"ref":"refs/heads/gh-readonly-queue/master/pr-2243-d970b781bc90b081ba35161d16661a56ee9666f7","pushedAt":"2024-06-05T16:03:34.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"}},{"before":"d970b781bc90b081ba35161d16661a56ee9666f7","after":"b13a032851a99c0abd9ebc55748ad0cbd1e0060d","ref":"refs/heads/master","pushedAt":"2024-06-05T16:03:32.000Z","pushType":"merge_queue_merge","commitsCount":1,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"Adds `Relation.Nullary.Recomputable` plus consequences (#2243)\n\n* prototype for fixing #2199\n\n* delegate to `Relation.Nullary.Negation.Core.weak-contradiction`\n\n* refactoring: lift out `Recomputable` in its own right\n\n* forgot to add this module\n\n* refactoring: tweak\n\n* tidying up; added `CHANGELOG`\n\n* more tidying up\n\n* streamlined `import`s\n\n* removed `Recomputable` from `Relation.Nullary`\n\n* fixed multiple definitions in `Relation.Unary`\n\n* reorder `CHANGELOG` entries after merge\n\n* `contradiciton` via `weak-contradiction`\n\n* irrefutable `with`\n\n* use `of`\n\n* only use *irrelevant* `⊥-elim-irr`\n\n* tightened `import`s\n\n* removed `irr-contradiction`\n\n* inspired by #2329\n\n* conjecture: all uses of `contradiction` can be made weak\n\n* second thoughts: reverted last round of chnages\n\n* lazier pattern analysis cf. #2055\n\n* dependencies: uncoupled from `Recomputable`\n\n* moved `⊥` and `¬ A` properties to this one place\n\n* removed `contradictionᵒ` and rephrased everything in terms of `weak-contradiction`\n\n* knock-on consequences; simplified `import`s\n\n* narrow `import`s\n\n* narrow `import`s; irrefutable `with`\n\n* narrow `import`s; `CHANGELOG`\n\n* narrow `import`s\n\n* response to review comments\n\n* irrelevance of `recompute`\n\n* knock-on, plus proof of `UIP` from #2149\n\n* knock-ons from renaming\n\n* knock-on from renaming\n\n* pushed proof `recompute-constant` to `Recomputable`","shortMessageHtmlLink":"Adds <code>Relation.Nullary.Recomputable</code> plus consequences (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2062419217\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/agda-stdlib/issues/2243\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/agda-stdlib/pull/2243/hovercard\" href=\"https://github.com/agda/agda-stdlib/pull/2243\">#2243</a>)"}},{"before":null,"after":"c0fafe970d46f64ebd755a854c7c91b41fd2993f","ref":"refs/heads/gh-readonly-queue/master/pr-2324-b13a032851a99c0abd9ebc55748ad0cbd1e0060d","pushedAt":"2024-06-05T15:46:22.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"Refactor `List.Membership.*` and `List.Relation.Unary.Any` (#2324)\n\n* `contradiction` against `⊥-elim`\n\n* tightened `import`s\n\n* added two operations `∃∈` and `∀∈`\n\n* added to `CHANGELOG`\n\n* knock-on for the `Propositional` case\n\n* refactor `lose∘find` and `find∘lose` in terms of new lemmas `∃∈-Any∘find` and `find∘∃∈-Any`\n\n* `CHANGELOG`\n\n* reorder\n\n* knock-on viscosity\n\n* knock-on viscosity; plus refactoring of `×↔` for intelligibility\n\n* knock-on viscosity\n\n* tightened `import`s\n\n* misc. import and other tweaks\n\n* misc. import and other tweaks\n\n* misc. import and other tweaks\n\n* removed spurious module name\n\n* better definition of `find`\n\n* make intermediate terms explicit in proof of `to∘from`\n\n* tweaks\n\n* Update Setoid.agda\n\nRemove redundant import of `index` from `Any`\n\n* Update Setoid.agda\n\nRemoved more redundant `import`ed operations\n\n* Update Properties.agda\n\nAnother redundant `import`\n\n* Update Properties.agda\n\nAnother redundant `import`ed operation\n\n* `with` into `let`\n\n* `with` into `let`\n\n* `with` into `let`\n\n* `with` into `let`\n\n* indentation\n\n* fix `universal-U`\n\n* added `map-cong`\n\n* deprecate `map-compose` in favour of `map-∘`\n\n* explicit `let` in statement of `find∘map`\n\n* knock-on viscosity: hide `map-cong`\n\n* use of `Product.map₁`\n\n* revert use of `Product.map₁`\n\n* inlined lemmas!\n\n* alpha conversion and further inlining!\n\n* correctted use of `Product.map₂`\n\n* added `syntax` declarations for the new combinators\n\n* remove`⊥-elim`\n\n* reordered `CHANGELOG`\n\n* revise combinator names\n\n* tighten `import`s\n\n* tighten `import`s\n\n* fixed merge conflict bug\n\n* removed new syntax\n\n* knock-on","shortMessageHtmlLink":"Refactor <code>List.Membership.*</code> and <code>List.Relation.Unary.Any</code> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2200010236\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/agda-stdlib/issues/2324\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/agda-stdlib/pull/2324/hovercard\" href=\"https://github.com/agda/agda-stdlib/pull/2324\">#2324</a>)"}},{"before":"3cbef5f3081a1cd391477e7389b95b31ada52287","after":"2857149def8e6b1273d0259d394e28a2ad57300b","ref":"refs/heads/gh-pages","pushedAt":"2024-06-05T15:32:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/agda-stdlib@d970b781bc90b081ba35161d16661a56ee9666f7 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/agda-stdlib/commit/d970b781bc90b081ba35161d16661a56ee9666f7/hovercard\" href=\"https://github.com/agda/agda-stdlib/commit/d970b781bc90b081ba35161d16661a56ee9666f7\"><tt>d970b78</tt></a> 🚀"}},{"before":null,"after":"b13a032851a99c0abd9ebc55748ad0cbd1e0060d","ref":"refs/heads/gh-readonly-queue/master/pr-2243-d970b781bc90b081ba35161d16661a56ee9666f7","pushedAt":"2024-06-05T15:28:27.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"Adds `Relation.Nullary.Recomputable` plus consequences (#2243)\n\n* prototype for fixing #2199\n\n* delegate to `Relation.Nullary.Negation.Core.weak-contradiction`\n\n* refactoring: lift out `Recomputable` in its own right\n\n* forgot to add this module\n\n* refactoring: tweak\n\n* tidying up; added `CHANGELOG`\n\n* more tidying up\n\n* streamlined `import`s\n\n* removed `Recomputable` from `Relation.Nullary`\n\n* fixed multiple definitions in `Relation.Unary`\n\n* reorder `CHANGELOG` entries after merge\n\n* `contradiciton` via `weak-contradiction`\n\n* irrefutable `with`\n\n* use `of`\n\n* only use *irrelevant* `⊥-elim-irr`\n\n* tightened `import`s\n\n* removed `irr-contradiction`\n\n* inspired by #2329\n\n* conjecture: all uses of `contradiction` can be made weak\n\n* second thoughts: reverted last round of chnages\n\n* lazier pattern analysis cf. #2055\n\n* dependencies: uncoupled from `Recomputable`\n\n* moved `⊥` and `¬ A` properties to this one place\n\n* removed `contradictionᵒ` and rephrased everything in terms of `weak-contradiction`\n\n* knock-on consequences; simplified `import`s\n\n* narrow `import`s\n\n* narrow `import`s; irrefutable `with`\n\n* narrow `import`s; `CHANGELOG`\n\n* narrow `import`s\n\n* response to review comments\n\n* irrelevance of `recompute`\n\n* knock-on, plus proof of `UIP` from #2149\n\n* knock-ons from renaming\n\n* knock-on from renaming\n\n* pushed proof `recompute-constant` to `Recomputable`","shortMessageHtmlLink":"Adds <code>Relation.Nullary.Recomputable</code> plus consequences (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2062419217\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/agda-stdlib/issues/2243\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/agda-stdlib/pull/2243/hovercard\" href=\"https://github.com/agda/agda-stdlib/pull/2243\">#2243</a>)"}},{"before":"fb0296685ade3b01eded148fc4e4b9d8c1faca76","after":"3cbef5f3081a1cd391477e7389b95b31ada52287","ref":"refs/heads/gh-pages","pushedAt":"2024-06-05T15:21:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/agda-stdlib@7306dff77b66ae51d71a125bad767fb13b5a238c 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/agda-stdlib/commit/7306dff77b66ae51d71a125bad767fb13b5a238c/hovercard\" href=\"https://github.com/agda/agda-stdlib/commit/7306dff77b66ae51d71a125bad767fb13b5a238c\"><tt>7306dff</tt></a> 🚀"}},{"before":"5e5fa2361036f2377aa684e3b5b7f04a76ae106f","after":"fb0296685ade3b01eded148fc4e4b9d8c1faca76","ref":"refs/heads/gh-pages","pushedAt":"2024-06-05T15:07:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ agda/agda-stdlib@17c84f401c25ec898b1853dbf1ce9d0e5a608911 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/agda/agda-stdlib/commit/17c84f401c25ec898b1853dbf1ce9d0e5a608911/hovercard\" href=\"https://github.com/agda/agda-stdlib/commit/17c84f401c25ec898b1853dbf1ce9d0e5a608911\"><tt>17c84f4</tt></a> 🚀"}},{"before":"d970b781bc90b081ba35161d16661a56ee9666f7","after":null,"ref":"refs/heads/gh-readonly-queue/master/pr-2366-7306dff77b66ae51d71a125bad767fb13b5a238c","pushedAt":"2024-06-05T14:57:04.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"}},{"before":"7306dff77b66ae51d71a125bad767fb13b5a238c","after":"d970b781bc90b081ba35161d16661a56ee9666f7","ref":"refs/heads/master","pushedAt":"2024-06-05T14:57:04.000Z","pushType":"merge_queue_merge","commitsCount":1,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"Improve `Data.List.Base` (fix #2359; deprecate use of with #2123) (#2366)\n\n* refactor towards `if_then_else_`\n\n* layout\n\n* `let` into `where`","shortMessageHtmlLink":"Improve <code>Data.List.Base</code> (<span class=\"issue-keyword tooltipped tooltipped-se\" aria-label=\"This commit closes issue #2359.\">fix</span> <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2238935156\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/agda-stdlib/issues/2359\" data-hovercard-type=\"issue\" data-hovercard-url=\"/agda/agda-stdlib/issues/2359/hovercard\" href=\"https://github.com/agda/agda-stdlib/issues/2359\">#2359</a>; deprecate use of with <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1927662801\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/agda-stdlib/issues/2123\" data-hovercard-type=\"issue\" data-hovercard-url=\"/agda/agda-stdlib/issues/2123/hovercard\" href=\"https://github.com/agda/agda-stdlib/issues/2123\">#2123</a>) (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2244043813\" data-permission-text=\"Title is private\" data-url=\"https://github.com/agda/agda-stdlib/issues/2366\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/agda/agda-stdlib/pull/2366/hovercard\" href=\"https://github.com/agda/agda-stdlib/pull/2366\">#2366</a>"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEYEWk8QA","startCursor":null,"endCursor":null}},"title":"Activity · agda/agda-stdlib"}