diff --git a/.github/workflows/ci-nix.yml b/.github/workflows/ci-nix.yml
new file mode 100644
index 0000000000..bfd033ed2a
--- /dev/null
+++ b/.github/workflows/ci-nix.yml
@@ -0,0 +1,18 @@
+name: Nix
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    paths:
+      - '**.nix'
+      - 'flake.lock'
+
+jobs:
+  deploy:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+      - uses: cachix/install-nix-action@v17
+      - name: Build
+        run:  nix build -v --print-build-logs
diff --git a/INSTALL.md b/INSTALL.md
index 19b5e2031f..7bb5ee00d3 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -282,3 +282,42 @@ cubical
 $ cat .agda/libraries
 /path/to/cubical.agda-lib
 ```
+
+Nix flakes instructions
+=======================
+
+Create a nix flake like this one:
+```nix
+{
+  inputs.cubical = {
+    url = "github:agda/cubical";
+    inputs.nixpkgs.follows = "nixpkgs";
+  };
+  outputs = { self, nixpkgs, cubical }:
+  let system = "x86_64-linux";
+      cub-packages = cubical.packages.${system};
+      cubical-lbry = cub-packages.cubical;
+  in
+  with import nixpkgs { system = system; };
+  rec {
+    packages.${system} = {
+      cubical = cubical-lbry;
+      agda = agda.withPackages [cubical-lbry];
+    };
+    defaultPackage.${system} = packages.${system}.agda;
+  };
+}
+```
+cubical-lbry is the cubical library that you have to add in Agda packages.
+
+You can test if Agda with the cubical library is working after adding this file:
+`test.agda`
+```agda
+{-# OPTIONS --cubical #-}
+open import Cubical.Foundations.Prelude
+```
+And running:
+```shell
+nix --extra-experimental-features "nix-command flakes" shell
+agda -l cubical -i . test.agda
+```
diff --git a/RELEASE.md b/RELEASE.md
index 43100ccd61..067fb86eae 100644
--- a/RELEASE.md
+++ b/RELEASE.md
@@ -14,3 +14,7 @@ Post-release
    include: .
    depend:
   ```
+
+* Increment the `version` field in `flake.nix`.
+
+* Update flake inputs by running `nix flake update`.
diff --git a/default.nix b/default.nix
new file mode 100644
index 0000000000..2cccff28d5
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,10 @@
+(import
+  (
+    let lock = builtins.fromJSON (builtins.readFile ./flake.lock); in
+    fetchTarball {
+      url = "https://github.com/edolstra/flake-compat/archive/${lock.nodes.flake-compat.locked.rev}.tar.gz";
+      sha256 = lock.nodes.flake-compat.locked.narHash;
+    }
+  )
+  { src = ./.; }
+).defaultNix
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000000..0b22aa608d
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,59 @@
+{
+  "nodes": {
+    "flake-compat": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1668681692,
+        "narHash": "sha256-Ht91NGdewz8IQLtWZ9LCeNXMSXHUss+9COoqu6JLmXU=",
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "rev": "009399224d5e398d03b22badca40a37ac85412a1",
+        "type": "github"
+      },
+      "original": {
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "type": "github"
+      }
+    },
+    "flake-utils": {
+      "locked": {
+        "lastModified": 1652557277,
+        "narHash": "sha256-jSes9DaIVMdmwBB78KkFUVrlDzawmD62vrUg0GS2500=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "12806d31a381e7cd169a6bac35590e7b36dc5fe5",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1661239106,
+        "narHash": "sha256-C5OCLnrv2c4CHs9DMEtYKkjJmGL7ySAZ1PqPkHBonxQ=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "963d27a0767422be9b8686a8493dcade6acee992",
+        "type": "github"
+      },
+      "original": {
+        "id": "nixpkgs",
+        "ref": "nixpkgs-unstable",
+        "type": "indirect"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-compat": "flake-compat",
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000000..fb982df5fc
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,54 @@
+{
+  description = "Cubical Agda";
+
+  inputs.nixpkgs.url = "nixpkgs/nixpkgs-unstable";
+  inputs.flake-utils.url = "github:numtide/flake-utils";
+  inputs.flake-compat = {
+    url = "github:edolstra/flake-compat";
+    flake = false;
+  };
+
+  outputs = { self, flake-compat, flake-utils, nixpkgs }:
+    let
+      inherit (nixpkgs.lib) cleanSourceWith hasSuffix;
+      overlay = final: prev: {
+        cubical = final.agdaPackages.mkDerivation rec {
+          pname = "cubical";
+          version = "0.4";
+
+          src = cleanSourceWith {
+            filter = name: type:
+              !(hasSuffix ".nix" name)
+            ;
+            src = ./.;
+          };
+
+
+          LC_ALL = "C.UTF-8";
+
+          # The cubical library has several `Everything.agda` files, which are
+          # compiled through the make file they provide.
+          nativeBuildInputs = [ final.ghc ];
+          buildPhase = ''
+            make
+          '';
+          meta = {
+            description = "An experimental library for Cubical Agda";
+            homepage = "https://github.com/agda/cubical";
+            license = "MIT License";
+          };
+        };
+        agdaWithCubical = final.agdaPackages.agda.withPackages [final.cubical];
+      };
+      overlays = [ overlay ];
+    in
+    { overlays.default = overlay; } //
+    flake-utils.lib.eachDefaultSystem (system:
+      let pkgs = import nixpkgs { inherit system overlays; };
+      in rec {
+        packages = with pkgs; rec {
+          inherit cubical agdaWithCubical;
+          default = cubical;
+        };
+      });
+}