diff --git a/.gitignore b/.gitignore
index 5179e47f6..c9d7a56d3 100644
--- a/.gitignore
+++ b/.gitignore
@@ -127,3 +127,6 @@ setup.log
 
 # Local OPAM switch
 _opam/
+
+# for Nix
+result/
\ No newline at end of file
diff --git a/README.md b/README.md
index 81520bc89..7ba317085 100644
--- a/README.md
+++ b/README.md
@@ -11,11 +11,16 @@ by Gratzer, Sterling, and Birkedal. Code has been incorporated from
 [redtt](https://www.github.com/RedPRL/redtt), implemented by Sterling and
 Favonia.
 
-## building
+A small collection of example programs is contained in the `test/` directory.
+See `test/README.md` for a brief description of each program's purpose.
+
+## Building
 
 cooltt has been built with OCaml 4.13.0 with [opam
-2.0.8](https://opam.ocaml.org/). If you are running an older version of OCaml,
-try executing the following command:
+2.0.8](https://opam.ocaml.org/). 
+
+### With OPAM
+If you are running an older version of OCaml, try executing the following command:
 
 ```
 $ opam switch create 4.13.0
@@ -40,9 +45,24 @@ $ make upgrade-pins                     # update and upgrade dependencies in act
 $ dune exec cooltt                      # from the `cooltt` top-level directory
 ```
 
+### With Nix
+First, you'll need the [Nix package manager](https://nixos.org/download.html), and then
+you'll need to [install or enable flakes](https://nixos.wiki/wiki/Flakes).
 
-A small collection of example programs is contained in the `test/` directory.
-See `test/README.md` for a brief description of each program's purpose.
+Then, cooltt can be built with the command
+```
+nix build --impure
+```
+to put a binary `cooltt` in `result/bin/cooltt`. This is good for if you just want to build
+and play around with cooltt.
+
+If you're working on cooltt, you can enter a development shell with an OCaml compiler, dune,
+and other tools with
+```
+nix develop --impure
+```
+and then build as in the [with OPAM](https://github.com/RedPRL/cooltt/#with-opam=) section 
+above.
 
 ## Acknowledgments
 
diff --git a/cooltt.opam b/cooltt.opam
index 9527eff4f..b572f19b9 100644
--- a/cooltt.opam
+++ b/cooltt.opam
@@ -26,7 +26,7 @@ depends: [
 ]
 pin-depends: [
   [ "kado.~dev" "git+https://github.com/RedPRL/kado" ]
-  [ "bantorra.0.1.0" "git+https://github.com/RedPRL/bantorra#0.1.0" ]
+  [ "bantorra.0.1.0" "git+https://github.com/RedPRL/bantorra#1e78633d9a2ef7104552a24585bb8bea36d4117b" ]
 ]
 build: [
   ["dune" "build" "-p" name "-j" jobs]
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 000000000..dba74585f
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,139 @@
+{
+  "nodes": {
+    "flake-compat": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1627913399,
+        "narHash": "sha256-hY8g6H2KFL8ownSiFeMOjwPC8P0ueXpCVEbxgda3pko=",
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "rev": "12c64ca55c1014cdc1b16ed5a804aa8576601ff2",
+        "type": "github"
+      },
+      "original": {
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "type": "github"
+      }
+    },
+    "flake-utils": {
+      "locked": {
+        "lastModified": 1656928814,
+        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1656947410,
+        "narHash": "sha256-htDR/PZvjUJGyrRJsVqDmXR8QeoswBaRLzHt13fd0iY=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "e8d47977286a44955262adbc76f2c8a66e7419d5",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-22.05",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs_2": {
+      "locked": {
+        "lastModified": 1640418986,
+        "narHash": "sha256-a8GGtxn2iL3WAkY5H+4E0s3Q7XJt6bTOvos9qqxT5OQ=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "5c37ad87222cfc1ec36d6cd1364514a9efc2f7f2",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "opam-nix": {
+      "inputs": {
+        "flake-compat": "flake-compat",
+        "flake-utils": [
+          "flake-utils"
+        ],
+        "nixpkgs": [
+          "nixpkgs"
+        ],
+        "opam-repository": [
+          "opam-repository"
+        ],
+        "opam2json": "opam2json"
+      },
+      "locked": {
+        "lastModified": 1657048488,
+        "narHash": "sha256-hoR9viiz3DxXGglZcntR2/b5DKCVOcBQfAenRG3j/JY=",
+        "owner": "tweag",
+        "repo": "opam-nix",
+        "rev": "0f1ccb994f625639f31c17273b757439f0944242",
+        "type": "github"
+      },
+      "original": {
+        "owner": "tweag",
+        "repo": "opam-nix",
+        "type": "github"
+      }
+    },
+    "opam-repository": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1657035053,
+        "narHash": "sha256-Vgt3iBauMn9xgB8iK0Gxzy+2rG/Q2GwsTNtOFl5UKXQ=",
+        "owner": "ocaml",
+        "repo": "opam-repository",
+        "rev": "2c86e8475c5f034ded996d82642b63d4551d6dcd",
+        "type": "github"
+      },
+      "original": {
+        "owner": "ocaml",
+        "repo": "opam-repository",
+        "type": "github"
+      }
+    },
+    "opam2json": {
+      "inputs": {
+        "nixpkgs": "nixpkgs_2"
+      },
+      "locked": {
+        "lastModified": 1651529032,
+        "narHash": "sha256-fe8bm/V/4r2iNxgbitT2sXBqDHQ0GBSnSUSBg/1aXoI=",
+        "owner": "tweag",
+        "repo": "opam2json",
+        "rev": "e8e9f2fa86ef124b9f7b8db41d3d19471c1d8901",
+        "type": "github"
+      },
+      "original": {
+        "owner": "tweag",
+        "repo": "opam2json",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs",
+        "opam-nix": "opam-nix",
+        "opam-repository": "opam-repository"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 000000000..d92937e22
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,36 @@
+{
+  description = "Experimental implementation of Cartesian cubical type theory";
+
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-22.05";
+    flake-utils.url = "github:numtide/flake-utils";
+
+    opam-repository = {
+      url = "github:ocaml/opam-repository";
+      flake = false;
+    };
+    
+    opam-nix = {
+      url = "github:tweag/opam-nix";
+      inputs.nixpkgs.follows = "nixpkgs";
+      inputs.flake-utils.follows = "flake-utils";
+      inputs.opam-repository.follows = "opam-repository";
+    };
+  };
+
+  outputs = { self
+            , flake-utils
+            , opam-nix
+            , nixpkgs
+            , opam-repository
+            }@inputs:
+    flake-utils.lib.eachDefaultSystem (system: {
+      legacyPackages = let
+        on = opam-nix.lib.${system};
+      in on.buildDuneProject { } "cooltt" ./. {
+        ocaml-base-compiler = null;
+      };
+
+      defaultPackage = self.legacyPackages.${system}."cooltt";
+    });
+}