diff --git a/docs/agda-spec/src/Interface/HasOrder/Instance.agda b/docs/agda-spec/src/Interface/HasOrder/Instance.agda
index 71fde50e9b..96fe482e37 100644
--- a/docs/agda-spec/src/Interface/HasOrder/Instance.agda
+++ b/docs/agda-spec/src/Interface/HasOrder/Instance.agda
@@ -26,10 +26,6 @@ instance
 
   open import Data.Rational using (ℚ)
   import Data.Rational.Properties as Rat hiding (_≟_)
-
-  ℚ-Dec-≤ = ⁇² Rat._≤?_
-  ℚ-Dec-< = ⁇² Rat._<?_
-
   ℚ-hasPreorder = hasPreorderFromNonStrict Rat.≤-isPreorder _≟_
   ℚ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Rat.≤-antisym }
   ℚ-hasDecPartialOrder = HasDecPartialOrder {A = ℚ} ∋ record {}
diff --git a/docs/agda-spec/src/Tactic/ByEq.agda b/docs/agda-spec/src/Tactic/ByEq.agda
deleted file mode 100644
index 4743808dce..0000000000
--- a/docs/agda-spec/src/Tactic/ByEq.agda
+++ /dev/null
@@ -1,56 +0,0 @@
-{-# OPTIONS --safe --without-K #-}
-module Tactic.ByEq where
-
-open import Prelude
-open import PreludeMeta
-open import Class.Functor.Core; open import Class.Functor.Instances
-open import Class.Monad.Core; open import Class.Monad.Instances
-
--- Introduce as many arguments as possible and then:
---   1. for those of type `_ ≡ _`, unify with  `refl`
---   2. ignore the rest of the arguments (unify with `_`)
---   3. unify the hole with `refl`
-by-eq : Hole → TC ⊤
-by-eq hole = do
-  ty ← withNormalisation true $ inferType hole
-  let ps : Args Pattern
-      ps = argTys ty <&> fmap λ {(def (quote _≡_) _) → quote refl ◇; _ → dot unknown}
-  unify hole $ pat-lam [ clause [] ps (quote refl ◆) ] []
-
-macro $by-eq = by-eq
-
-private
-  -- test that macro works
-  _ : ∀ {n m k : ℕ} → n ≡ m → m ≡ k → n ≡ k
-  _ = $by-eq
-
-  _ : ∀ {n m k x y : ℕ} → n ≡ m → x ≡ y → m ≡ n
-  _ = $by-eq
-
-  -- test that tactic arguments work
-  f : {@(tactic by-eq) _ : ∀ {n m : ℕ} → n ≡ m → m ≡ n} → Bool → Bool
-  f = id
-
-  _ : f {λ where refl → refl} true ≡ true
-  _ = refl
-
-  _ : f {$by-eq} true ≡ true
-  _ = refl
-
-  _ : f true ≡ true
-  _ = refl
-
-  -- test that normalisation works
-  Sym = ∀ {n m : ℕ} → n ≡ m → m ≡ n
-
-  g : {@(tactic by-eq) _ : Sym} → Bool → Bool
-  g = id
-
-  _ : g {λ where refl → refl} true ≡ true
-  _ = refl
-
-  _ : g {$by-eq} true ≡ true
-  _ = refl
-
-  _ : g true ≡ true
-  _ = refl
diff --git a/flake.lock b/flake.lock
index f90219a450..1540541897 100644
--- a/flake.lock
+++ b/flake.lock
@@ -35,11 +35,11 @@
     },
     "agda-nixpkgs": {
       "locked": {
-        "lastModified": 1716802541,
-        "narHash": "sha256-J2WSefw1i2GJDNGC3E6F8Mr9/iOzB+EfVT52g+Rqz6s=",
+        "lastModified": 1726583932,
+        "narHash": "sha256-zACxiQx8knB3F8+Ze+1BpiYrI+CbhxyWpcSID9kVhkQ=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "7148a46c2a1163faecb2915f5f1e6e6c43bcd3ee",
+        "rev": "658e7223191d2598641d50ee4e898126768fe847",
         "type": "github"
       },
       "original": {
diff --git a/nix/agda.nix b/nix/agda.nix
index ffaef2a9d4..03f91165c9 100644
--- a/nix/agda.nix
+++ b/nix/agda.nix
@@ -21,10 +21,10 @@ let
     pname = "agda-stdlib-classes";
     version = "2.0";
     src = pkgs.fetchFromGitHub {
-      repo = "agda-stdlib-classes";
       owner = "omelkonian";
+      repo = "agda-stdlib-classes";
       rev = "v2.0";
-      sha256 = "4ujdQv38u6BybFhRup9PMR0xpI59J/Naz/kaBtQQ9aY=";
+      hash = "sha256-PcieRRnctjCzFCi+gUYAgyIAicMOAZPl8Sw35fZdt0E=";
     };
     meta = { };
     libraryFile = "agda-stdlib-classes.agda-lib";
@@ -37,10 +37,10 @@ let
     pname = "agda-stdlib-meta";
     version = "2.0";
     src = pkgs.fetchFromGitHub {
-      repo = "stdlib-meta";
-      owner = "input-output-hk";
-      rev = "4fc4b1ed6e47d180516917d04be87cbacbf7d314";
-      sha256 = "T+9vwccbDO1IGBcGLjgV/fOt+IN14KEV9ct/J6nQCsM=";
+      owner = "omelkonian";
+      repo = "agda-stdlib-meta";
+      rev = "v2.1.1";
+      hash = "sha256-qOoThYMG0dzjKvwmzzVZmGcerfb++MApbaGRzLEq3/4=";
     };
     meta = { };
     libraryFile = "agda-stdlib-meta.agda-lib";