diff --git a/dotfiles/init.el b/dotfiles/init.el
index 3cb9b966..98d94554 100644
--- a/dotfiles/init.el
+++ b/dotfiles/init.el
@@ -34,8 +34,6 @@
     (local-set-key (kbd "C-n") 'comint-next-input)
     ))
 
-(require 'agda2)
-
 (require 'bind-key)
 ; (bind-key* "M-p" 'pixel-scroll-down)
 ; (bind-key* "M-n" 'pixel-scroll-up)
@@ -154,16 +152,5 @@
 (put 'upcase-region 'disabled nil)
 (put 'narrow-to-region 'disabled nil)
 
-(require 'agda-input)
-
-(setq agda-input-tweak-all
-      '(agda-input-compose
-        (agda-input-prepend "!")
-        (agda-input-nonempty))
-      )
-(agda-input-setup)
-
-(setq default-input-method "Agda")
-(add-to-list 'auto-mode-alist '("\\.lagda.md\\'" . agda2-mode))
 
 ; (setq ring-bell-function (lambda () (call-process "sh" nil 0 nil "-c" "find /Users/xenia/cloud/configs/resources -type f | egrep -v '/_' | shuf -n 1 | xargs afplay")))
diff --git a/flake.lock b/flake.lock
index f1b32973..f18cec6c 100644
--- a/flake.lock
+++ b/flake.lock
@@ -1,27 +1,5 @@
 {
   "nodes": {
-    "agda": {
-      "inputs": {
-        "flake-parts": "flake-parts",
-        "nixpkgs": [
-          "nixpkgs"
-        ]
-      },
-      "locked": {
-        "lastModified": 1723809509,
-        "narHash": "sha256-aC0Vc/YV+rodv1qG839rqNFBqoqy/AkgvLdHxymCIu4=",
-        "owner": "agda",
-        "repo": "agda",
-        "rev": "df1a26d96683ebb06aa8476e4af6bbeddf23efbe",
-        "type": "github"
-      },
-      "original": {
-        "owner": "agda",
-        "ref": "v2.7.0",
-        "repo": "agda",
-        "type": "github"
-      }
-    },
     "ansi-utils": {
       "inputs": {
         "flake-utils": "flake-utils",
@@ -58,24 +36,6 @@
         "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"
@@ -177,11 +137,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1718222105,
-        "narHash": "sha256-3hyVDQNIue0N505XlUGu9piUBlOYMPWaUk/iycVgNsU=",
+        "lastModified": 1733339173,
+        "narHash": "sha256-TGhQugZKrxz3Su5wcfC/muBwbPK2z8kGEdRzjUM1baY=",
         "ref": "refs/heads/main",
-        "rev": "2da2cf21138f7de8e4238049f7bb3cdd97db9286",
-        "revCount": 10457,
+        "rev": "fc30e5e21fc6e8e2135ae164cd353a13501e643c",
+        "revCount": 10465,
         "type": "git",
         "url": "https://githug.xyz/xenia/kakoune.git"
       },
@@ -246,24 +206,6 @@
         "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-unstable": {
       "locked": {
         "lastModified": 1733097829,
@@ -298,7 +240,6 @@
     },
     "root": {
       "inputs": {
-        "agda": "agda",
         "ansi-utils": "ansi-utils",
         "home-manager": "home-manager",
         "kak": "kak",
diff --git a/flake.nix b/flake.nix
index 4e531185..b38cc514 100644
--- a/flake.nix
+++ b/flake.nix
@@ -32,10 +32,6 @@
       url = "git+https://git@githug.xyz/xenia/unambig-path";
       inputs.nixpkgs.follows = "nixpkgs";
     };
-    agda = {
-      url = "github:agda/agda?ref=v2.7.0";
-      inputs.nixpkgs.follows = "nixpkgs";
-    };
     nixos-apple-silicon = {
       url = "github:tpwrules/nixos-apple-silicon";
       # TODO: when nixos-24.11 drops, change this
@@ -43,7 +39,7 @@
     };
   };
 
-  outputs = { self, nixpkgs, nixpkgs-unstable, home-manager, nix-darwin, kak, unispect, ansi-utils, unambig-path, agda, nixos-apple-silicon }:
+  outputs = { self, nixpkgs, nixpkgs-unstable, home-manager, nix-darwin, kak, unispect, ansi-utils, unambig-path, nixos-apple-silicon }:
     let
       mkPkgs = system: import nixpkgs { system = system; config.allowUnfree = true; };
       mkPkgsUnstable = system: import nixpkgs-unstable { system = system; config.allowUnfree = true; };
@@ -55,11 +51,9 @@
         unispect = unispect.packages.${system}.unispect;
         ansi-utils = ansi-utils.packages.${system};
         unambig-path = unambig-path.packages.${system}.unambig-path;
-        agda = agda.packages.${system}.default;
       };
       mkPC = {system, pkgs} : import ./home/graphical.nix {
         inherit pkgs;
-        agda = agda.packages.${system}.default;
       };
       mkLaptop = {system, pkgs} : import ./home/apps.nix {
         inherit pkgs;
diff --git a/home/common.nix b/home/common.nix
index c459ea72..99c9cb07 100644
--- a/home/common.nix
+++ b/home/common.nix
@@ -1,4 +1,4 @@
-{ pkgs, username, home-dir, prompt-color, kak-pkg, unispect, ansi-utils, unambig-path, agda }:
+{ pkgs, username, home-dir, prompt-color, kak-pkg, unispect, ansi-utils, unambig-path }:
 
 let
   kak = import ./kak.nix { kak = kak-pkg; inherit pkgs; };
@@ -12,8 +12,7 @@ in rec {
   home.stateVersion = "23.05";
 
   home.packages =
-    [ agda ] ++ (with pkgs.agdaPackages; [ standard-library cubical ])
-  ++ extras.all ++ (with pkgs; [
+    extras.all ++ (with pkgs; [
     # Terminal utilities
     unispect
     ansi-utils.ansicols
diff --git a/home/graphical.nix b/home/graphical.nix
index 061bd772..1852caea 100644
--- a/home/graphical.nix
+++ b/home/graphical.nix
@@ -1,4 +1,4 @@
-{ pkgs, agda }:
+{ pkgs }:
 
 let
   alacritty = import ./alacritty/alacritty.nix pkgs;
@@ -16,28 +16,6 @@ let
       cp -r Alloy.app $out/Applications
     '';
   };
-  agda2-mode = pkgs.emacsPackages.trivialBuild {
-    pname = "agda-mode";
-    version = agda.version;
-
-    dontUnpack = true;
-
-    # already byte-compiled by Agda builder
-    buildPhase = ''
-      agda=`${agda}/bin/agda-mode locate`
-      cp `dirname $agda`/*.el* .
-    '';
-
-    meta = {
-      inherit (agda.meta) homepage license;
-      description = "Agda2-mode for Emacs extracted from Agda package";
-      longDescription = ''
-        Wrapper packages that liberates init.el from `agda-mode locate` magic.
-        Simply add this to user profile or systemPackages and do `(require
-        'agda2)` in init.el.
-      '';
-    };
-  };
 
 in rec {
   home.packages = with pkgs; [
@@ -52,7 +30,7 @@ in rec {
   programs.emacs = {
     package = pkgs.emacs;
     enable = true;
-    extraPackages = epkgs: [agda2-mode] ++ (with epkgs; [
+    extraPackages = epkgs: (with epkgs; [
       vterm bind-key rust-mode lsp-mode company meow haskell-mode
       terraform-mode nix-mode insert-kaomoji
     ]);