diff --git a/.envrc b/.envrc
index e69de29..3550a30 100644
--- a/.envrc
+++ b/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/flake.lock b/flake.lock
index f9f141b..133a80a 100644
--- a/flake.lock
+++ b/flake.lock
@@ -1,5 +1,42 @@
 {
   "nodes": {
+    "agda": {
+      "inputs": {
+        "flake-parts": "flake-parts",
+        "nixpkgs": "nixpkgs"
+      },
+      "locked": {
+        "lastModified": 1719426791,
+        "narHash": "sha256-jiPGzJM+XMwb1OwyxpbY6jV0Lzr5yLKnPSMZbueFNRM=",
+        "owner": "agda",
+        "repo": "agda",
+        "rev": "777b07f573c7526d677c18c25e44b24a849bc03b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "agda",
+        "repo": "agda",
+        "type": "github"
+      }
+    },
+    "flake-parts": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib"
+      },
+      "locked": {
+        "lastModified": 1701473968,
+        "narHash": "sha256-YcVE5emp1qQ8ieHUnxt1wCZCC3ZfAS+SRRWZ2TMda7E=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "34fed993f1674c8d06d58b37ce1e0fe5eebcb9f5",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
     "flake-utils": {
       "inputs": {
         "systems": "systems"
@@ -18,6 +55,40 @@
       }
     },
     "nixpkgs": {
+      "locked": {
+        "lastModified": 1702346276,
+        "narHash": "sha256-eAQgwIWApFQ40ipeOjVSoK4TEHVd6nbSd9fApiHIw5A=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "cf28ee258fd5f9a52de6b9865cdb93a1f96d09b7",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-23.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-lib": {
+      "locked": {
+        "dir": "lib",
+        "lastModified": 1701253981,
+        "narHash": "sha256-ztaDIyZ7HrTAfEEUt9AtTDNoCYxUdSd6NrRHaYOIxtk=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "e92039b55bcd58469325ded85d4f58dd5a4eaf58",
+        "type": "github"
+      },
+      "original": {
+        "dir": "lib",
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs_2": {
       "locked": {
         "lastModified": 1718089647,
         "narHash": "sha256-COO4Xk2EzlZ3x9KCiJildlAA6cYDSPlnY8ms7pKl2Iw=",
@@ -33,8 +104,9 @@
     },
     "root": {
       "inputs": {
+        "agda": "agda",
         "flake-utils": "flake-utils",
-        "nixpkgs": "nixpkgs"
+        "nixpkgs": "nixpkgs_2"
       }
     },
     "systems": {
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..eaeff5a
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,19 @@
+{
+  inputs.agda.url = "github:agda/agda";
+  outputs = { self, nixpkgs, flake-utils, agda }: flake-utils.lib.eachDefaultSystem (system:
+    let
+      pkgs = import nixpkgs { inherit system; };
+      agda-pkg = agda.packages.x86_64-linux.default;
+      flakePkgs = {
+        agda = agda-pkg;
+        agda-bin = pkgs.callPackage ./nix/agda-bin.nix { agda = agda-pkg; };
+        docker-builder = pkgs.callPackage ./nix/docker-builder.nix { };
+      };
+    in
+    {
+      packages = flake-utils.lib.flattenTree flakePkgs;
+      devShell = pkgs.mkShell {
+        packages = with pkgs; [ nixfmt-rfc-style ];
+      };
+    });
+}
diff --git a/nix/agda-bin.nix b/nix/agda-bin.nix
new file mode 100644
index 0000000..5c2ed45
--- /dev/null
+++ b/nix/agda-bin.nix
@@ -0,0 +1,6 @@
+{ agda, runCommand }:
+
+runCommand "agda-bin" { }
+  ''
+    cp ${agda}/bin/agda $out
+  ''
diff --git a/nix/agda.nix b/nix/agda.nix
new file mode 100644
index 0000000..c072dc6
--- /dev/null
+++ b/nix/agda.nix
@@ -0,0 +1,6 @@
+{ haskellPackages }:
+
+haskellPackages.developPackage {
+  name = "agda";
+  version = "2.6.4.3";
+}
diff --git a/nix/docker-builder.nix b/nix/docker-builder.nix
new file mode 100644
index 0000000..fbeb4f2
--- /dev/null
+++ b/nix/docker-builder.nix
@@ -0,0 +1,3 @@
+{ dockerTools }:
+
+dockerTools.buildImage { }