diff --git a/modules/lang/agda/README.org b/modules/lang/agda/README.org
new file mode 100644
index 000000000..1812f748d
--- /dev/null
+++ b/modules/lang/agda/README.org
@@ -0,0 +1,9 @@
+#+TITLE: :lang agda
+
+This module adds support for the [[http://wiki.portal.chalmers.se/agda/pmwiki.php][agda]] programming language.
+
+Emacs support is included in the agda release (you can find installation
+instructions [[https://agda.readthedocs.io/en/latest/getting-started/installation.html][here]]). This module attempts to find the location of ~agda2.el~ via
+the ~agda-mode locate~ command that comes with the agda release. Users can set
+this manually by setting the ~+agda2-dir~ variable. 
+
diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el
new file mode 100644
index 000000000..dc21ae25c
--- /dev/null
+++ b/modules/lang/agda/config.el
@@ -0,0 +1,38 @@
+;;; lang/agda/config.el -*- lexical-binding: t; -*-
+
+(defvar +agda-dir
+  (when (executable-find "agda-mode")
+    (file-name-directory (shell-command-to-string "agda-mode locate"))))
+
+(def-package! agda2
+  :when +agda-dir
+  :load-path +agda-dir)
+
+(def-package! agda2-mode
+  :defer t
+  :config
+  (map! :map agda2-mode-map
+        :localleader
+        :n "?"  #'agda2-show-goals
+        :n "."  #'agda2-goal-and-context-and-inferred
+        :n ","   #'agda2-goal-and-context
+        :n "="   #'agda2-show-constraints
+        :n "SPC" #'agda2-give
+        :n "a"   #'agda2-auto
+        :n "c"   #'agda2-make-case
+        :n "d"   #'agda2-infer-type-maybe-toplevel
+        :n "e"   #'agda2-show-context
+        :n "gG"  #'agda2-go-back
+        :n "h"   #'agda2-helper-function-type
+        :n "l"   #'agda2-load
+        :n "n"  #'agda2-compute-normalised-maybe-toplevel
+        :n "p"  #'agda2-module-contents-maybe-toplevel
+        :n "r"  #'agda2-refine
+        :n "s"  #'agda2-solveAll
+        :n "t"  #'agda2-goal-type
+        :n "w"  #'agda2-why-in-scope-maybe-toplevel
+        :n "xc" #'agda2-compile
+        :n "xd" #'agda2-remove-annotations
+        :n "xh" #'agda2-display-implicit-arguments
+        :n "xq" #'agda2-quit
+        :n "xr" #'agda2-restart))
diff --git a/modules/lang/agda/doctor.el b/modules/lang/agda/doctor.el
new file mode 100644
index 000000000..e38ccbc03
--- /dev/null
+++ b/modules/lang/agda/doctor.el
@@ -0,0 +1,5 @@
+;; -*- lexical-binding: t; no-byte-compile: t; -*-
+;;; lang/agda/doctor.el
+
+(unless (executable-find "agda-mode")
+  (warn! "Couldn't find agda-mode. Agda support won't work"))