diff --git a/README.md b/README.md
index f2f8b5a..3b16aa8 100644
--- a/README.md
+++ b/README.md
@@ -137,6 +137,10 @@ call cornelis#bind_input("nat", "ℕ")
 
 will add `<LocalLeader>nat` as an input remapping for `ℕ`.
 
+The inverse of `cornelis#bind_input("foo", "...")` is `cornelis#unbind_input("foo")`.
+Note that this cannot and will not attempt to undo any custom agda-input
+management, such as through `g:cornelis_bind_input_hook` (see below).
+
 
 #### Custom Hooks
 
diff --git a/autoload/cornelis.vim b/autoload/cornelis.vim
index cd04b22..3a9f6b0 100644
--- a/autoload/cornelis.vim
+++ b/autoload/cornelis.vim
@@ -35,3 +35,24 @@ function! cornelis#bind_input(key, result)
   endif
 endfunction
 
+function! cornelis#unbind_input(key) abort
+  let l:cornelis_agda_prefix = get(g:, 'cornelis_agda_prefix', '<localleader>')
+  let l:lhs = l:cornelis_agda_prefix . substitute(a:key, '|', '<bar>', 'g')
+
+  execute 'silent! iunmap <buffer> ' . l:lhs
+  execute 'silent! cunmap <buffer> ' . l:lhs
+
+  if exists('g:agda_input') && type(g:agda_input) == type({})
+    let l:first = a:key[0:0]
+    let l:rest  = (len(a:key) > 1) ? a:key[1:] : "\<CR>"
+
+    if has_key(g:agda_input, l:first)
+      if has_key(g:agda_input[l:first], l:rest)
+        call remove(g:agda_input[l:first], l:rest)
+      endif
+      if empty(g:agda_input[l:first])
+        call remove(g:agda_input, l:first)
+      endif
+    endif
+  endif
+endfunction