Merge branch 'master' into Bool-action

Author: jamesmckinna

.github/workflows/ci-ubuntu.yml

@@ -76,8 +76,7 @@ jobs:
           if [[ '${{ github.ref }}' == 'refs/heads/experimental' \
              || '${{ github.base_ref }}' == 'experimental' ]]; then
             # Pick Agda version for experimental
-            echo "AGDA_COMMIT=3d04bacca842729f9c0869b9287256321b5f450f" >> "${GITHUB_ENV}";
-              # Andreas, 2025-10-07: 3d04bacca842729f9c0869b9287256321b5f450f is tags/v2.8.0
+            echo "AGDA_COMMIT=tags/v2.8.0" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}"
           else
             # Pick Agda version for master
@@ -170,8 +169,7 @@ jobs:
 
       - name: Golden testing
         run: |
-          ${{ env.CABAL_V1_INSTALL }} clock
-          make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda'
+          make testsuite INTERACTIVE='' AGDA_EXEC='agda' GHC_EXEC='ghc'
 
 
 ########################################################################

.gitignore

@@ -27,6 +27,7 @@ GenerateEverything
 Haskell
 html
 log
+logs/
 MAlonzo
 output
 runtests

CHANGELOG.md

@@ -161,6 +161,20 @@ Additions to existing modules
   ⊕-∧-booleanRing   : BooleanRing _ _
   ```
 
+* In `Algebra.Module.Properties.LeftModule`:
+  ```agda
+  -1#*ₗm≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m
+  -‿distrib-*ₗ : ∀ r m → - r *ₗ m ≈ᴹ -ᴹ (r *ₗ m)
+  -ᴹ‿distrib-*ₗ : ∀ r m → r *ₗ (-ᴹ m) ≈ᴹ -ᴹ (r *ₗ m)
+  ```
+
+* In `Algebra.Module.Properties.RightModule`:
+  ```agda
+  -1#*ₗm≈-ᴹm : m*ᵣ-1#≈-ᴹm : ∀ m → m *ᵣ (- 1#) ≈ᴹ -ᴹ m
+  -‿distrib-*ᵣ : ∀ m r → m *ᵣ (- r) ≈ᴹ -ᴹ (m *ᵣ r)
+  -ᴹ‿distrib-*ᵣ : ∀ m r → (-ᴹ m) *ᵣ r ≈ᴹ -ᴹ (m *ᵣ r)
+  ```
+
 * In `Algebra.Properties.Monoid.Mult` properties of the Boolean action on a RawMonoid:
   ```agda
   ?>₀-homo-true  : true ?>₀ x ≈ x
@@ -333,6 +347,17 @@ Additions to existing modules
   [_]⊢_ : (A → B) → Pred A ℓ → Pred B _
   ```
 
+* In `Relation.Unary.Properties`
+  ```agda
+  _map-⊢_   : P ⊆ Q → f ⊢ P ⊆ f ⊢ Q
+  map-⟨_⟩⊢_ : P ⊆ Q → ⟨ f ⟩⊢ P ⊆ ⟨ f ⟩⊢ Q
+  map-[_]⊢_ : P ⊆ Q → [ f ]⊢ P ⊆ [ f ]⊢ Q
+  ⟨_⟩⊢⁻_    : ⟨ f ⟩⊢ P ⊆ Q → P ⊆ f ⊢ Q
+  ⟨_⟩⊢⁺_    : P ⊆ f ⊢ Q → ⟨ f ⟩⊢ P ⊆ Q
+  [_]⊢⁻_    : Q ⊆ [ f ]⊢ P → f ⊢ Q ⊆ P
+  [_]⊢⁺_    : f ⊢ Q ⊆ P → Q ⊆ [ f ]⊢ P
+  ```
+
 * In `System.Random`:
   ```agda
   randomIO : IO Bool

GNUmakefile

@@ -1,3 +1,4 @@
+GHC_EXEC ?= ghc
 AGDA_EXEC ?= agda
 AGDA_OPTIONS=-Werror
 AGDA_RTS_OPTIONS=+RTS -M4.0G -H3.5G -A128M -RTS
@@ -14,7 +15,7 @@ test: doc/Everything.agda check-whitespace
 	cd doc && $(AGDA) README.agda
 
 testsuite:
-	$(MAKE) -C tests test AGDA="$(AGDA)" AGDA_EXEC="$(AGDA_EXEC)" only=$(only)
+	$(MAKE) -C tests test GHC_EXEC="$(GHC_EXEC)" AGDA="$(AGDA)" only=$(only)
 
 fix-whitespace:
 	$(CABAL_EXEC) exec -- fix-whitespace

README.md

@@ -32,6 +32,17 @@ in glorious clickable HTML.
 
 ## Installation instructions
 
+### Automated installation (currently experimental)
+
+On Unix-style systems, it should be as simple as running the following command in
+a shell:
+
+```shell
+sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh)"
+```
+
+### Manual installation
+
 See the [installation instructions](https://github.com/agda/agda-stdlib/blob/master/doc/installation-guide.md) for the latest version of the standard library.
 
 #### Old versions of Agda

doc/installation-guide.md

@@ -3,6 +3,21 @@ Installation instructions
 
 Note: the full story on installing Agda libraries can be found at [readthedocs](http://agda.readthedocs.io/en/latest/tools/package-system.html).
 
+
+## Automated installation on Unix-style systems
+
+Running the following command in a terminal will download the
+[installation script](../stdlib-install.sh) and run it. It will
+ask you some questions about your setup and automatically install
+a version of the standard library compatible with your installed
+version of Agda.
+
+```shell
+sh -c "$(curl --proto '=https' --tlsv1.2 -s https://raw.githubusercontent.com/agda/agda-stdlib/refs/heads/master/stdlib-install.sh)"
+```
+
+## Manual installation
+
 Use version v2.3 of the standard library with Agda v2.8.0 or v2.7.0.1. You can find the correct version of the library to use for different Agda versions on the [Agda Wiki](https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary).
 
 1. Navigate to a suitable directory `$HERE` (replace appropriately) where

doc/release-guide.txt

@@ -57,6 +57,10 @@ procedure should be followed:
 * Submit a pull request to update the version of standard library on Homebrew
   (https://github.com/Homebrew/homebrew-core/blob/master/Formula/agda.rb)
 
+* Update the [install script](../stdlib-install.sh):
+
+  ** The big `case` block mapping Agda versions to stdlib versions
+
 * Update the Agda wiki:
 
   ** The standard library page.

src/Algebra/Module/Properties/LeftModule.agda

@@ -23,3 +23,27 @@ open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public
   renaming (inverseˡ-unique to inverseˡ-uniqueᴹ
            ; inverseʳ-unique to inverseʳ-uniqueᴹ
            ; ⁻¹-involutive to -ᴹ-involutive)
+
+open import Algebra.Properties.Ring ring
+
+open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid
+
+-‿distrib-*ₗ : ∀ r m → - r *ₗ m ≈ᴹ -ᴹ (r *ₗ m)
+-‿distrib-*ₗ r m = inverseʳ-uniqueᴹ (r *ₗ m) (- r *ₗ m) (begin
+  r *ₗ m +ᴹ - r *ₗ m ≈⟨ *ₗ-distribʳ m r (- r) ⟨
+  (r - r) *ₗ m       ≈⟨ *ₗ-congʳ (-‿inverseʳ r) ⟩
+  0# *ₗ m            ≈⟨ *ₗ-zeroˡ m ⟩
+  0ᴹ                 ∎)
+
+-ᴹ‿distrib-*ₗ : ∀ r m → r *ₗ (-ᴹ m) ≈ᴹ -ᴹ (r *ₗ m)
+-ᴹ‿distrib-*ₗ r m = inverseʳ-uniqueᴹ (r *ₗ m) (r *ₗ (-ᴹ m)) (begin
+    r *ₗ m +ᴹ r *ₗ (-ᴹ m) ≈⟨ *ₗ-distribˡ r m (-ᴹ m) ⟨
+    r *ₗ (m +ᴹ (-ᴹ m))    ≈⟨ *ₗ-congˡ (-ᴹ‿inverseʳ m) ⟩
+    r *ₗ 0ᴹ               ≈⟨ *ₗ-zeroʳ r ⟩
+    0ᴹ                    ∎)
+
+-1#*ₗm≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m
+-1#*ₗm≈-ᴹm m = begin
+  - 1# *ₗ m    ≈⟨ -‿distrib-*ₗ 1# m ⟩
+  -ᴹ (1# *ₗ m) ≈⟨ -ᴹ‿cong (*ₗ-identityˡ m) ⟩
+  -ᴹ m         ∎

src/Algebra/Module/Properties/RightModule.agda

@@ -23,3 +23,28 @@ open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public
   renaming (inverseˡ-unique to inverseˡ-uniqueᴹ
            ; inverseʳ-unique to inverseʳ-uniqueᴹ
            ; ⁻¹-involutive to -ᴹ-involutive)
+
+open import Algebra.Properties.Ring ring
+
+open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid
+
+-‿distrib-*ᵣ : ∀ m r → m *ᵣ (- r) ≈ᴹ -ᴹ (m *ᵣ r)
+-‿distrib-*ᵣ m r = inverseʳ-uniqueᴹ (m *ᵣ r) (m *ᵣ - r) (begin
+  m *ᵣ r +ᴹ m *ᵣ - r ≈⟨ *ᵣ-distribˡ m r (- r) ⟨
+  m *ᵣ (r - r)       ≈⟨ *ᵣ-congˡ (-‿inverseʳ r) ⟩
+  m *ᵣ 0#            ≈⟨ *ᵣ-zeroʳ m ⟩
+  0ᴹ                 ∎)
+
+-ᴹ‿distrib-*ᵣ : ∀ m r → (-ᴹ m) *ᵣ r ≈ᴹ -ᴹ (m *ᵣ r)
+-ᴹ‿distrib-*ᵣ m r = inverseʳ-uniqueᴹ (m *ᵣ r) ((-ᴹ m) *ᵣ r) (begin
+    m *ᵣ r +ᴹ (-ᴹ m) *ᵣ r ≈⟨ *ᵣ-distribʳ r m (-ᴹ m) ⟨
+    (m +ᴹ -ᴹ m) *ᵣ r      ≈⟨ *ᵣ-congʳ (-ᴹ‿inverseʳ m) ⟩
+    0ᴹ *ᵣ r               ≈⟨ *ᵣ-zeroˡ r ⟩
+    0ᴹ                    ∎)
+
+m*ᵣ-1#≈-ᴹm : ∀ m → m *ᵣ (- 1#) ≈ᴹ -ᴹ m
+m*ᵣ-1#≈-ᴹm m = begin
+  m *ᵣ (- 1#)  ≈⟨ -‿distrib-*ᵣ m 1# ⟩
+  -ᴹ (m *ᵣ 1#) ≈⟨ -ᴹ‿cong (*ᵣ-identityʳ m) ⟩
+  -ᴹ m         ∎
+

src/Function/Related/TypeIsomorphisms.agda

@@ -41,6 +41,7 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 open import Relation.Nullary.Negation.Core using (¬_)
 import Relation.Nullary.Indexed as I
+open import Relation.Unary.Properties using (⟨_⟩⊢⁻_; ⟨_⟩⊢⁺_)
 
 private
   variable
@@ -356,6 +357,6 @@ Related-cong {A = A} {B = B} {C = C} {D = D} A≈B C≈D = mk⇔
 -- restriction that the quantified variable is equal to the given one
 
 ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
-∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , refl , Py) → Py)
+∃-≡ P {x} = mk↔ₛ′ (⟨ id ⟩⊢⁻ id) (⟨ id ⟩⊢⁺ id)
   (λ where (_ , refl , _) → refl) (λ where _ → refl)