diff --git a/flake.lock b/flake.lock
index f116931..a7e41dc 100644
--- a/flake.lock
+++ b/flake.lock
@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1717285511,
-        "narHash": "sha256-iKzJcpdXih14qYVcZ9QC9XuZYnPc6T8YImb6dX166kw=",
+        "lastModified": 1736143030,
+        "narHash": "sha256-+hu54pAoLDEZT9pjHlqL9DNzWz0NbUn8NEAHP7PQPzU=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "2a55567fcf15b1b1c7ed712a2c6fadaec7412ea8",
+        "rev": "b905f6fc23a9051a6e1b741e1438dbfc0634c6de",
         "type": "github"
       },
       "original": {
@@ -21,11 +21,11 @@
     "formal-ledger": {
       "flake": false,
       "locked": {
-        "lastModified": 1718812337,
-        "narHash": "sha256-3zAxfOEs/Ff5g13493iZGGhcvYaSOJNkQLN/G3/AhiY=",
+        "lastModified": 1736958942,
+        "narHash": "sha256-KAyojB3uClt72fhOzw9iDSCGzlL8EUhEtK/Xizj5pyU=",
         "owner": "IntersectMBO",
         "repo": "formal-ledger-specifications",
-        "rev": "6129d97a0419f8d920e3ed63e192f34cbaf65cc6",
+        "rev": "cef3505f275900c51737071b5671e5dad47dc576",
         "type": "github"
       },
       "original": {
@@ -36,11 +36,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1718717814,
-        "narHash": "sha256-xB7AzKY4BP7yypo6g+sk1tnVK54sBIJMeEBB5CdbhT4=",
+        "lastModified": 1737223978,
+        "narHash": "sha256-5r5py5/ckGE7EzQk0uwOyeDus4xowRPmFrAhSNrb51g=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "88af533d8ae8d1e7e4648decf7817ebff91abf56",
+        "rev": "d37c24666dc05cdf1e9b76ea4437e3f222c7f944",
         "type": "github"
       },
       "original": {
@@ -51,14 +51,14 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1717284937,
-        "narHash": "sha256-lIbdfCsf8LMFloheeE6N31+BMIeixqyQWbSr2vk79EQ=",
+        "lastModified": 1735774519,
+        "narHash": "sha256-CewEm1o2eVAnoqb6Ml+Qi9Gg/EfNAxbRx1lANGVyoLI=",
         "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/eb9ceca17df2ea50a250b6b27f7bf6ab0186f198.tar.gz"
+        "url": "https://github.com/NixOS/nixpkgs/archive/e9b51731911566bbf7e4895475a87fe06961de0b.tar.gz"
       },
       "original": {
         "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/eb9ceca17df2ea50a250b6b27f7bf6ab0186f198.tar.gz"
+        "url": "https://github.com/NixOS/nixpkgs/archive/e9b51731911566bbf7e4895475a87fe06961de0b.tar.gz"
       }
     },
     "root": {
diff --git a/flake.nix b/flake.nix
index 443595e..254094c 100644
--- a/flake.nix
+++ b/flake.nix
@@ -25,6 +25,7 @@
           };
           agdaLibraries = with agdaPackages;
             [
+              abstract-set-theory
               formal-ledger
               standard-library
               standard-library-classes
diff --git a/hydra-protocol.agda-lib b/hydra-protocol.agda-lib
index 65c9e87..0215a73 100644
--- a/hydra-protocol.agda-lib
+++ b/hydra-protocol.agda-lib
@@ -1,5 +1,6 @@
 name: hydra-protocol
 depend:
+  abstract-set-theory
   formal-ledger
   standard-library
   standard-library-classes
diff --git a/nix/initial-packages.nix b/nix/initial-packages.nix
index 8240af5..ac86b55 100644
--- a/nix/initial-packages.nix
+++ b/nix/initial-packages.nix
@@ -17,6 +17,8 @@ let
 
       agda = withPackages [ ];
 
+      abstract-set-theory = callPackage ./pkgs/abstract-set-theory.nix { };
+
       formal-ledger = callPackage ./pkgs/formal-ledger.nix { };
 
       standard-library = callPackage ./pkgs/standard-library.nix { };
diff --git a/nix/pkgs/abstract-set-theory.nix b/nix/pkgs/abstract-set-theory.nix
new file mode 100644
index 0000000..6de4e18
--- /dev/null
+++ b/nix/pkgs/abstract-set-theory.nix
@@ -0,0 +1,22 @@
+{ lib, mkDerivation, fetchFromGitHub, standard-library, standard-library-classes, standard-library-meta }:
+
+mkDerivation rec {
+  version = "0.1.0";
+  pname = "abstract-set-theory";
+
+  src = (fetchFromGitHub {
+    owner = "input-output-hk";
+    repo = "agda-sets";
+    rev = "751b3ee39122fe33022af41e6c94dc820afde19a";
+    sha256 = "sha256-0vjmNN8wuZXT4NM3aEv4z1Y+/6LpNfb7vzeajwZ3eFY=";
+  });
+
+  buildInputs = [ standard-library standard-library-classes standard-library-meta ];
+
+  everythingFile = "src/abstract-set-theory.agda";
+
+  libraryFile = "abstract-set-theory.agda-lib";
+
+  meta = { };
+}
+
diff --git a/nix/pkgs/formal-ledger.nix b/nix/pkgs/formal-ledger.nix
index 65776b6..5140f02 100644
--- a/nix/pkgs/formal-ledger.nix
+++ b/nix/pkgs/formal-ledger.nix
@@ -1,17 +1,17 @@
-{ lib, mkDerivation, fetchFromGitHub, standard-library, standard-library-classes, standard-library-meta }:
+{ lib, mkDerivation, fetchFromGitHub, abstract-set-theory, standard-library, standard-library-classes, standard-library-meta }:
 
 mkDerivation rec {
   version = "0.2.0";
   pname = "formal-ledger";
 
   src = (fetchFromGitHub {
-    owner = "locallycompact";
+    owner = "IntersectMBO";
     repo = "formal-ledger-specifications";
-    rev = "d2a1746ec6671ee7699487ae41b97b275160e71a";
-    sha256 = "sha256-2G9VEimSLFm4j/LdM+khJ43jTRwc3q7eQEdY6w5KvD8=";
+    rev = "cef3505f275900c51737071b5671e5dad47dc576";
+    sha256 = "sha256-KAyojB3uClt72fhOzw9iDSCGzlL8EUhEtK/Xizj5pyU=";
   }) + "/src";
 
-  buildInputs = [ standard-library standard-library-classes standard-library-meta ];
+  buildInputs = [ abstract-set-theory standard-library standard-library-classes standard-library-meta ];
 
   meta = { };
 }
diff --git a/nix/pkgs/standard-library-classes.nix b/nix/pkgs/standard-library-classes.nix
index de04b7d..46fc13c 100644
--- a/nix/pkgs/standard-library-classes.nix
+++ b/nix/pkgs/standard-library-classes.nix
@@ -7,14 +7,14 @@ mkDerivation rec {
   src = fetchFromGitHub {
     owner = "omelkonian";
     repo = "agda-stdlib-classes";
-    rev = "v${version}";
-    sha256 = "sha256-PcieRRnctjCzFCi+gUYAgyIAicMOAZPl8Sw35fZdt0E=";
+    rev = "28df278381c94a25c54f6819524cd9f8cb99f092";
+    sha256 = "sha256-TdPJ3K4jyAIQgX1sUrqd0QeA72n2mkBVzlg8WfrqWWY=";
   };
 
   buildInputs = [ standard-library ];
 
   libraryFile = "agda-stdlib-classes.agda-lib";
-  everythingFile = "Classes.agda";
+  everythingFile = "standard-library-classes.agda";
 
   meta = { };
 }
diff --git a/nix/pkgs/standard-library-meta.nix b/nix/pkgs/standard-library-meta.nix
index a8ab52d..f09d2e2 100644
--- a/nix/pkgs/standard-library-meta.nix
+++ b/nix/pkgs/standard-library-meta.nix
@@ -1,14 +1,14 @@
 { lib, mkDerivation, fetchFromGitHub, standard-library, standard-library-classes }:
 
 mkDerivation rec {
-  version = "2.0";
+  version = "2.1.1";
   pname = "agda-stdlib-meta";
 
   src = fetchFromGitHub {
-    owner = "input-output-hk";
-    repo = "stdlib-meta";
-    rev = "4fc4b1ed6e47d180516917d04be87cbacbf7d314";
-    sha256 = "T+9vwccbDO1IGBcGLjgV/fOt+IN14KEV9ct/J6nQCsM=";
+    owner = "agda";
+    repo = "agda-stdlib-meta";
+    rev = "v${version}";
+    sha256 = "sha256-qOoThYMG0dzjKvwmzzVZmGcerfb++MApbaGRzLEq3/4=";
   };
 
   buildInputs = [ standard-library standard-library-classes ];
diff --git a/nix/pkgs/standard-library.nix b/nix/pkgs/standard-library.nix
index 9779277..a9315c3 100644
--- a/nix/pkgs/standard-library.nix
+++ b/nix/pkgs/standard-library.nix
@@ -1,17 +1,23 @@
-{ lib, mkDerivation, fetchFromGitHub, ghcWithPackages, nixosTests }:
+{
+  lib,
+  mkDerivation,
+  fetchFromGitHub,
+  ghcWithPackages,
+  nixosTests,
+}:
 
 mkDerivation rec {
   pname = "standard-library";
-  version = "2.0";
+  version = "2.1.1";
 
   src = fetchFromGitHub {
     repo = "agda-stdlib";
     owner = "agda";
     rev = "v${version}";
-    hash = "sha256-TjGvY3eqpF+DDwatT7A78flyPcTkcLHQ1xcg+MKgCoE=";
+    hash = "sha256-4HfwNAkIhk1yC/oSxZ30xilzUM5/22nzbUSqTjcW5Ng=";
   };
 
-  nativeBuildInputs = [ (ghcWithPackages (self : [ self.filemanip ])) ];
+  nativeBuildInputs = [ (ghcWithPackages (self: [ self.filemanip ])) ];
   preConfigure = ''
     runhaskell GenerateEverything.hs --include-deprecated
     # We will only build/consider Everything.agda, in particular we don't want Everything*.agda
@@ -25,6 +31,11 @@ mkDerivation rec {
     description = "Standard library for use with the Agda compiler";
     license = lib.licenses.mit;
     platforms = lib.platforms.unix;
-    maintainers = with maintainers; [ jwiegley mudri alexarice turion ];
+    maintainers = with maintainers; [
+      jwiegley
+      mudri
+      alexarice
+      turion
+    ];
   };
 }