[M1-1] Upgrade to Agda 2.8.0 and stdlib v2.3; replace `--without-K` with `--cubical-compatible`

[williamdemeo]

Description

The library is currently pinned to Agda 2.6.2 / stdlib 1.7. The Agda ecosystem has moved on: the current stable is Agda 2.8.0 (July 2025) and stdlib v2.3. --without-K has been superseded by --cubical-compatible since Agda 2.6.3. This issue tracks the full upgrade. Blocks essentially every other issue in this project.

Tasks

• Update agda-algebras.agda-lib to depend: standard-library-2.3 and document the minimum Agda version as 2.8.0.
• Replace every {-# OPTIONS --without-K --exact-split --safe #-} with {-# OPTIONS --cubical-compatible --exact-split --safe #-}.
• Fix any regressions from the flag change.
• Update import paths for anything that moved between stdlib 1.7 and 2.3 (expected hotspots: Function.Bundles, Relation.Binary.* renamings, Data.* reorganizations).
• Update CI config to test against Agda 2.8.0 / stdlib 2.3.
• Update README.md and INSTALL.md to reflect the new requirements.
• Update the Nix flake.

Acceptance criteria

• Library type-checks under Agda 2.8.0 / stdlib v2.3.
• make check succeeds locally.
• No file still declares --without-K.
• Once 2.0 is stable, consider adding a CI job against Agda 2.9/dev to catch forward-compatibility issues early.