From 080eae2adc1b0e8f1829c4138b3d462218a02f36 Mon Sep 17 00:00:00 2001 From: Josselin Poiret Date: Sun, 30 Apr 2023 09:32:59 +0200 Subject: [PATCH 1/2] Bump Agda to 2.6.3 and stdlib to 1.7.2 --- .github/workflows/ci-ubuntu.yml | 4 ++-- agda-categories.agda-lib | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index ab26835d6..256044206 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -45,8 +45,8 @@ on: ######################################################################## env: - AGDA_COMMIT: tags/v2.6.2 - STDLIB_VERSION: 1.7.1 + AGDA_COMMIT: tags/v2.6.3 + STDLIB_VERSION: 1.7.2 GHC_VERSION: 8.6.5 CABAL_VERSION: 3.2.0.0 diff --git a/agda-categories.agda-lib b/agda-categories.agda-lib index 186e350b1..5b19c405e 100644 --- a/agda-categories.agda-lib +++ b/agda-categories.agda-lib @@ -1,3 +1,3 @@ name: agda-categories -depend: standard-library-1.7.1 +depend: standard-library-1.7.2 include: src/ From 992da3d1d17236c5f44095125b340f17ab5a366e Mon Sep 17 00:00:00 2001 From: Josselin Poiret Date: Thu, 4 May 2023 20:43:07 +0200 Subject: [PATCH 2/2] Update README for 0.1.8. --- README.md | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/README.md b/README.md index 87b89f9d0..b7e982732 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ Welcome to what will hopefully become the standard Category Theory library for Agda. -The current library release, v0.1.7, works with Agda-2.6.2 and stdlib-1.7.1. The master +The current library release, v0.1.8, works with Agda-2.6.3 and stdlib-1.7.2. The master branch should also work with same, but may contain various incompatibilities. Note that this should be considered pre-beta software, and that backwards compability @@ -68,10 +68,6 @@ Some of the lower-level design decisions (naming conventions, organization) are documented in the proto-contributor's guide. ### Some design decisions -- The library relies on eta expansion of records. However, due to a bug in Agda - 2.6.0.1, we need to switch this on in related records. In the next release of Agda, - hopefully we can remove these switches. See also [this agda - issue](https://github.com/agda/agda/issues/4142). - We add `sym-assoc` and `identity²` in order to achieve better definitional equality of `Category`. The rationale can be found in [this paper](https://arxiv.org/pdf/1401.7694.pdf).