diff --git a/.config/nvim/ftplugin/agda.vim b/.config/nvim/ftplugin/agda.vim
index 6a5dbec8..74a49940 100644
--- a/.config/nvim/ftplugin/agda.vim
+++ b/.config/nvim/ftplugin/agda.vim
@@ -2,34 +2,23 @@
 " https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VIMEditing#:~:text=agda%2Dutf8%2Evim
 " (Link is dead so use wayback machine)
 
-" To add more
-" https://www.compart.com/en/unicode/
-
 " Superscripts
-imap <buffer> \^0 ⁰
-imap <buffer> \^1 ¹
-imap <buffer> \^2 ²
-imap <buffer> \^3 ³
-imap <buffer> \^4 ⁴
-imap <buffer> \^5 ⁵
-imap <buffer> \^6 ⁶
-imap <buffer> \^7 ⁷
-imap <buffer> \^8 ⁸
-imap <buffer> \^9 ⁹
-imap <buffer> \^+ ⁺
-imap <buffer> \^- ⁻
-imap <buffer> \^= ⁼
-imap <buffer> \^( ⁽
-imap <buffer> \^) ⁾
-imap <buffer> \^n ⁿ
-
-imap <buffer> \^l ˡ
-imap <buffer> \^r ʳ
-
-imap <buffer> \' ′
-imap <buffer> \'' ″
-imap <buffer> \''' ‴
-imap <buffer> \'''' ⁗
+imap <buffer> ^0 ⁰
+imap <buffer> ^1 ¹
+imap <buffer> ^2 ²
+imap <buffer> ^3 ³
+imap <buffer> ^4 ⁴
+imap <buffer> ^5 ⁵
+imap <buffer> ^6 ⁶
+imap <buffer> ^7 ⁷
+imap <buffer> ^8 ⁸
+imap <buffer> ^9 ⁹
+imap <buffer> ^+ ⁺
+imap <buffer> ^- ⁻
+imap <buffer> ^= ⁼
+imap <buffer> ^( ⁽
+imap <buffer> ^) ⁾
+imap <buffer> ^n ⁿ
 
 " Subscripts
 imap <buffer> \_0 ₀
@@ -161,7 +150,26 @@ imap <buffer> \Chi Χ
 imap <buffer> \Psi Ψ
 imap <buffer> \Omega Ω
 
-" default cornelis mapping
+" autoload
+function! CornelisLoadWrapper()
+  if exists(":CornelisLoad") ==# 2
+    CornelisLoad
+  endif
+endfunction
+
+au BufReadPre *.agda call CornelisLoadWrapper()
+au BufReadPre *.lagda* call CornelisLoadWrapper()
+
+au BufRead,BufNewFile *.agda call AgdaFiletype()
+au BufRead,BufNewFile *.lagda* call AgdaFiletype()
+au QuitPre *.agda :CornelisCloseInfoWindows
+au QuitPre *.lagda* :CornelisCloseInfoWindows
+
+" autoreload at file write
+au BufWritePost *.agda execute "normal! :CornelisLoad\<CR>"
+au BufWritePost *.lagda* execute "normal! :CornelisLoad\<CR>"
+
+" default cornelis config
 nnoremap <buffer> <leader>l :CornelisLoad<CR>
 nnoremap <buffer> <leader>r :CornelisRefine<CR>
 nnoremap <buffer> <leader>d :CornelisMakeCase<CR>
diff --git a/.config/nvim/plugin/cornelis.vim b/.config/nvim/plugin/cornelis.vim
deleted file mode 100644
index 27930283..00000000
--- a/.config/nvim/plugin/cornelis.vim
+++ /dev/null
@@ -1,17 +0,0 @@
-" agda related autocommands
-
-function! CornelisLoadWrapper()
-  if exists(":CornelisLoad") ==# 2
-    CornelisLoad
-  endif
-endfunction
-
-au BufReadPre *.agda call CornelisLoadWrapper()
-au BufReadPre *.lagda* call CornelisLoadWrapper()
-
-au QuitPre *.agda :CornelisCloseInfoWindows
-au QuitPre *.lagda* :CornelisCloseInfoWindows
-
-" autoreload at file write
-au BufWritePost *.agda execute "normal! :CornelisLoad\<CR>"
-au BufWritePost *.lagda* execute "normal! :CornelisLoad\<CR>"
diff --git a/nix/overlays/cornelis.nix b/nix/overlays/cornelis.nix
index 3008001b..7ae3c175 100644
--- a/nix/overlays/cornelis.nix
+++ b/nix/overlays/cornelis.nix
@@ -2,9 +2,4 @@
 let
   sources = import ../../npins;
 in
-
-# If this is updated, we break split on case support for PLFA.
-# PLFA uses 2.7.0
-# https://github.com/agda/cornelis/issues/169
-assert sources.cornelis.version == "v2.7.1";
 sources.cornelis.asFlake.overlays.cornelis
diff --git a/nix/overlays/iosevka/default.nix b/nix/overlays/iosevka/default.nix
index bae060fa..236e7059 100644
--- a/nix/overlays/iosevka/default.nix
+++ b/nix/overlays/iosevka/default.nix
@@ -29,18 +29,18 @@ let
 
   identityOverlay = _: _: { };
   overlays =
-    let
-      # Useless complexity just for the fun
-      n-airyToList = acc: x: {
-        value = acc ++ [ x ];
-        __functor = self: n-airyToList self.value;
-      };
-      combinations = lib.crossLists (n-airyToList [ ]) [
+    lib.crossLists
+      (
+        spacingCfg: variantCfg:
+        lib.composeManyExtensions [
+          spacingCfg
+          variantCfg
+        ]
+      )
+      [
         (import ./spacings.nix)
         ([ identityOverlay ] ++ import ./variants.nix)
       ];
-    in
-    map ({ value, ... }: lib.composeManyExtensions value) combinations;
 
   iosevkas = lib.genAttrs' overlays (
     overlay:
diff --git a/npins/sources.json b/npins/sources.json
index c6de909e..929ec7c3 100644
--- a/npins/sources.json
+++ b/npins/sources.json
@@ -27,11 +27,10 @@
       "version_upper_bound": null,
       "release_prefix": null,
       "submodules": false,
-      "version": "v2.7.1",
-      "revision": "40298eed11eb877526b3ab3f648d8a7bff9e2f50",
-      "url": "https://api.github.com/repos/agda/cornelis/tarball/refs/tags/v2.7.1",
-      "hash": "sha256-h18AeggnOSSjy0RLJIkWsSID1BJTarOV9F1APKusIrE=",
-      "frozen": true
+      "version": "v2.8.0",
+      "revision": "67137c76fe0d4a8bb899eea46afaa370993d3556",
+      "url": "https://api.github.com/repos/agda/cornelis/tarball/refs/tags/v2.8.0",
+      "hash": "sha256-dGS6De3EtTirgEMDMSjA+iBNc670W7pG4eA02Nq7Azo="
     },
     "disko": {
       "type": "GitRelease",