diff --git a/nvim/.config/nvim/lua/options.lua b/nvim/.config/nvim/lua/options.lua
index c035d93..fbe552d 100644
--- a/nvim/.config/nvim/lua/options.lua
+++ b/nvim/.config/nvim/lua/options.lua
@@ -23,6 +23,10 @@ opt.conceallevel = 2
 opt.breakindent = true
 opt.linebreak = true
 
+opt.foldmethod = 'marker'
+-- opt.foldmethod = 'expr'
+-- opt.foldexpr = 'nvim_treesitter#foldexpr()'
+
 vim.api.nvim_create_autocmd('TermOpen', {
     pattern = '*',
     callback = function()
diff --git a/nvim/.config/nvim/lua/plugins/keys.lua b/nvim/.config/nvim/lua/plugins/keys.lua
index e8c68e0..231a4b0 100644
--- a/nvim/.config/nvim/lua/plugins/keys.lua
+++ b/nvim/.config/nvim/lua/plugins/keys.lua
@@ -3,21 +3,14 @@ return {
         'folke/which-key.nvim',
         event = 'VeryLazy',
         config = function()
-            -- set up groups
+            -- set up some groups
             local wk = require('which-key')
             wk.add({
                 { '<leader>f', group = 'find' },
                 { '<leader>h', group = 'help' },
+                { '<leader>e', group = 'explore' },
+                { '<leader>ee', ':Lexplore<CR>', desc='netrw cwd' },
             })
         end,
-        keys = {
-            {
-                "<leader>?",
-                function()
-                    require("which-key").show({ global = false })
-                end,
-                desc = "Buffer Local Keymaps (which-key)",
-            },
-        },
     }
 }
diff --git a/nvim/.config/nvim/lua/plugins/languages/agda.lua b/nvim/.config/nvim/lua/plugins/languages/agda.lua
new file mode 100644
index 0000000..72e141f
--- /dev/null
+++ b/nvim/.config/nvim/lua/plugins/languages/agda.lua
@@ -0,0 +1,10 @@
+return {
+    {
+        'isovector/cornelis',
+        dependencies = {
+            'kana/vim-textobj-user',
+            'neovimhaskell/nvim-hs.vim',
+        },
+        build = 'stack build',
+    }
+}
diff --git a/nvim/.config/nvim/lua/plugins/languages/coq.lua b/nvim/.config/nvim/lua/plugins/languages/coq.lua
index c863d59..12aef56 100644
--- a/nvim/.config/nvim/lua/plugins/languages/coq.lua
+++ b/nvim/.config/nvim/lua/plugins/languages/coq.lua
@@ -5,14 +5,21 @@ return {
         init = function()
             vim.g.loaded_coqtail = 1
             vim.g['coqtail#supported'] = 0
+            vim.cmd([[call digraph_set('|-', '⊢')]])
         end
     },
     {
-        'tomtomjhj/coq-lsp.nvim',
-        event = { 'BufReadPre *.v', 'BufNewFile *.v' },
-        opts = {
-            autostart = true,
-        },
-        dependencies = { 'whonore/Coqtail' }
+        'tomtomjhj/vscoq.nvim',
+        event = { 'BufReadPre *.v', 'BufNewFile *.v'},
+        opts = true,
+        dependencies = { 'whonore/Coqtail' },
     }
+    -- {
+    --     'tomtomjhj/coq-lsp.nvim',
+    --     event = { 'BufReadPre *.v', 'BufNewFile *.v' },
+    --     opts = {
+    --         autostart = true,
+    --     },
+    --     dependencies = { 'whonore/Coqtail' }
+    -- }
 }
diff --git a/nvim/.config/nvim/lua/plugins/languages/idris.lua b/nvim/.config/nvim/lua/plugins/languages/idris.lua
new file mode 100644
index 0000000..c99275b
--- /dev/null
+++ b/nvim/.config/nvim/lua/plugins/languages/idris.lua
@@ -0,0 +1,80 @@
+return {
+    {
+        'ShinKage/idris2-nvim',
+        event = { 'BufReadPre *.idr', 'BufNewFile *.idr' },
+        dependencies = {
+            'neovim/nvim-lspconfig',
+            'MunifTanjim/nui.nvim',
+            'folke/which-key.nvim'
+        },
+        config = function()
+            local wk = require('which-key')
+            local action = require('idris2.code_action')
+            local hover = require('idris2.hover')
+            local meta = require('idris2.metavars')
+            local browse = require('idris2.browse')
+            local repl = require('idris2.repl')
+
+            require('idris2').setup({
+                client = {
+                    hover = {
+                        use_split = false,
+                        split_size = '30%',
+                        auto_resize_split = false,
+                        split_position = 'bottom',
+                        with_history = true,
+                    },
+                },
+                autostart_semantic = true,
+                code_action_post_hook = save_hook,
+                use_default_semantic_hl_groups = true,
+                server = {
+                    init_options = {
+                        logFile = "~/.cache/idris2-lsp/server.log",
+                        longActionTimeout = 2000,
+                    },
+                    on_attach = function(...)
+                        wk.add({
+                            { '<leader>c', action.case_split, desc = 'Split case' },
+
+                            { '<leader>i', group = 'idris action' },
+                            { '<leader>ic', action.make_case, desc = 'Make case' },
+                            { '<leader>iw', action.make_with, desc = 'Make with' },
+                            { '<leader>il', action.make_lemma, desc = 'Make lemma' },
+                            { '<leader>ia', action.add_clause, desc = 'Add clause' },
+                            { '<leader>io', action.expr_search, desc = 'Expr search' },
+                            { '<leader>ig', action.generate_def, desc = 'Generate definition' },
+                            { '<leader>ir', action.refine_hole, desc = 'Refine hole' },
+                            { '<leader>ib', browse.browse, desc = 'Browse' },
+
+                            { '<leader>s', group = 'idris split' },
+                            { '<leader>so', hover.open_split, desc = 'Open' },
+                            { '<leader>sc', hover.close_split, desc = 'Close' },
+
+                            { '<leader>m', group = 'idris metavariables' },
+                            { '<leader>mm', meta.request_all, desc = 'Request all' },
+                            { '<leader>mn', meta.goto_next, desc = 'Next' },
+                            { '<leader>mp', meta.goto_prev, desc = 'Previous' },
+
+                            { '<leader>e', group = 'idris evaluate' },
+                            { '<leader>ee', repl.evaluate, desc = 'Expression' },
+                            {
+                                '<leader>ev',
+                                function() repl.evaluate({ visual = true}) end,
+                                desc = 'Visual selection',
+                                mode = 'v',
+                                group = 'idris evaluate'
+                            },
+                            {
+                                '<leader>er',
+                                function() repl.evaluate({ visual = true, sub = true}) end,
+                                desc = 'Replace selection',
+                                mode = 'v'
+                            },
+                        })
+                    end
+                }
+            })
+        end
+    }
+}
diff --git a/nvim/.config/nvim/lua/plugins/languages/mizar.lua b/nvim/.config/nvim/lua/plugins/languages/mizar.lua
new file mode 100644
index 0000000..8fd52ba
--- /dev/null
+++ b/nvim/.config/nvim/lua/plugins/languages/mizar.lua
@@ -0,0 +1,5 @@
+return {
+    {
+        'andy-morris/mizar.vim',
+    }
+}
diff --git a/nvim/.config/nvim/lua/plugins/languages/perga.lua b/nvim/.config/nvim/lua/plugins/languages/perga.lua
new file mode 100644
index 0000000..17b8465
--- /dev/null
+++ b/nvim/.config/nvim/lua/plugins/languages/perga.lua
@@ -0,0 +1,7 @@
+return {
+    {
+        -- "https://forgejo.ballcloud.cc/wball/perga.nvim",
+        url = "/home/wball/repos/perga.nvim",
+        config = true,
+    },
+}
diff --git a/nvim/.config/nvim/lua/plugins/lsp.lua b/nvim/.config/nvim/lua/plugins/lsp.lua
index d0ca1ed..b4187c5 100644
--- a/nvim/.config/nvim/lua/plugins/lsp.lua
+++ b/nvim/.config/nvim/lua/plugins/lsp.lua
@@ -13,10 +13,14 @@ return {
             vim.api.nvim_create_autocmd('LspAttach', {
                 group = vim.api.nvim_create_augroup('UserLspConfig', {}),
                 callback = function(ev)
+                    local builtin = require('telescope.builtin')
                     wk.add({
                         { 'gD', vim.lsp.buf.declaration, desc = 'Go to declaration' },
+                        { 'gR', builtin.lsp_references, desc = 'Go to references' },
+                        { 'gd', builtin.lsp_definitions, desc = 'Go to definition' },
 
-                        { '<leader>la', vim.lsp.buf.code_action, desc = 'See available code actions' },
+                        { '<leader>l', group = 'lsp' },
+                        { '<leader>la', vim.lsp.buf.code_action, desc = 'Code actions' },
                         { '<leader>lr', vim.lsp.buf.rename, desc = 'Rename' },
                         { '<leader>lf', vim.lsp.buf.format, desc = 'Format' },
                         { '<leader>le', vim.diagnostic.open_float, desc = 'Show line diagnostics' },
diff --git a/nvim/.config/nvim/lua/plugins/telescope.lua b/nvim/.config/nvim/lua/plugins/telescope.lua
index 0f8253b..39d9515 100644
--- a/nvim/.config/nvim/lua/plugins/telescope.lua
+++ b/nvim/.config/nvim/lua/plugins/telescope.lua
@@ -25,52 +25,52 @@ return {
             {
                 "<leader>ff",
                 require('telescope.builtin').find_files,
-                desc = 'Telescope find files'
+                desc = 'find files'
             },
             {
                 "<leader>fg",
                 require('telescope.builtin').live_grep,
-                desc = 'Telescope live grep'
+                desc = 'live grep'
             },
             {
                 "<leader>fb",
                 require('telescope.builtin').buffers,
-                desc = 'Telescope buffers'
+                desc = 'buffers'
             },
             {
                 "<leader>fh",
                 require('telescope.builtin').help_tags,
-                desc = 'Telescope help tags'
+                desc = 'help tags'
             },
             {
                 "<leader>fo",
                 require('telescope.builtin').oldfiles,
-                desc = 'Telescope old files'
+                desc = 'old files'
             },
             {
                 "<leader>fc",
                 require('telescope.builtin').commands,
-                desc = 'Telescope commands'
+                desc = 'commands'
             },
             {
                 "<leader>fm",
                 require('telescope.builtin').marks,
-                desc = 'Telescope marks'
+                desc = 'marks'
             },
             {
                 "<leader>fq",
                 require('telescope.builtin').quickfix,
-                desc = 'Telescope quickfix'
+                desc = 'quickfix'
             },
             {
                 "<leader>fl",
                 require('telescope.builtin').loclist,
-                desc = 'Telescope loclist'
+                desc = 'loclist'
             },
             {
                 "<leader>fr",
                 require('telescope.builtin').registers,
-                desc = 'Telescope registers'
+                desc = 'registers'
             },
         }
     },
diff --git a/nvim/.config/nvim/lua/plugins/utils.lua b/nvim/.config/nvim/lua/plugins/utils.lua
index 983a32c..69569a3 100644
--- a/nvim/.config/nvim/lua/plugins/utils.lua
+++ b/nvim/.config/nvim/lua/plugins/utils.lua
@@ -23,8 +23,8 @@ return {
             local neogit = require('neogit')
             wk.add({
                 { '<leader>g', group = 'git' },
-                { '<leader>gn', neogit.open, desc = 'Neogit' },
-                { '<leader>gd', ':DiffviewOpen<CR>', desc = 'Diffview' },
+                { '<leader>gn', neogit.open, desc = 'neogit' },
+                { '<leader>gd', ':DiffviewOpen<CR>', desc = 'diffview' },
             })
             neogit.setup({})
         end,
@@ -51,5 +51,36 @@ return {
 
             cmp.event:on('confirm_done', cmp_autopairs.on_confirm_done())
         end
+    },
+    {
+        'akinsho/toggleterm.nvim',
+        version = '*',
+        event = 'VeryLazy',
+        opts = {
+            open_mapping = [[<C-\>]]
+        }
+    },
+    {
+        'numToStr/Navigator.nvim',
+        config = function()
+            local navigator = require('Navigator')
+            vim.keymap.set({'n', 't'}, '<A-h>', navigator.left)
+            vim.keymap.set({'n', 't'}, '<A-j>', navigator.down)
+            vim.keymap.set({'n', 't'}, '<A-k>', navigator.up)
+            vim.keymap.set({'n', 't'}, '<A-l>', navigator.right)
+            vim.keymap.set({'n', 't'}, '<A-p>', navigator.previous)
+            navigator.setup()
+        end
+    },
+    {
+        'echasnovski/mini.align',
+        version = false,
+        opts = {
+            -- modifiers = {
+            --     i = function(steps, _)
+            --         table.insert(steps.pre_split, align.gen_step.ignore_split({ '".-"', "'.-'", '(.-)' }))
+            --     end
+            -- }
+        }
     }
 }