diff --git a/contrib/lang/agda/README.md b/contrib/lang/agda/README.md
new file mode 100644
index 000000000..fa220aa92
--- /dev/null
+++ b/contrib/lang/agda/README.md
@@ -0,0 +1,56 @@
+# Agda contribution layer for Spacemacs
+
+## Description
+
+This layer adds support for the [Agda][] programming language.
+
+Some features:
+- Faces redefined to correctly play with themes.
+- Spacemacs bindings to Agda's interactive tools.
+
+**This layer is in construction, it needs your contributions and bug reports.**
+
+## Install
+
+### Layer
+
+To use this contribution add it to your `~/.spacemacs`
+
+```elisp
+(setq-default dotspacemacs-configuration-layers '(agda))
+```
+
+### Agda
+
+This layer requires Agda to be installed, and available on the `PATH` as seen by Emacs.
+
+## Key bindings
+
+All Agda specific bindings are prefixed with the major-mode leader
+<kbd>SPC m</kbd>.
+
+Top-level commands are prefixed by <kbd>SPC m</kbd>:
+
+    Key Binding       |                 Description
+----------------------|------------------------------------------------------------
+<kbd>SPC m l</kbd>    | Load current buffer.
+<kbd>SPC m a</kbd>    | Simple proof search.
+<kbd>SPC m r</kbd>    | Refine the goal at point.
+<kbd>SPC m s</kbd>    | Solves all goals that are already instantiated internally.
+<kbd>SPC m t</kbd>    | Show the type of the goal at point.
+<kbd>SPC m c</kbd>    | Refine the pattern variables given in the goal.
+<kbd>SPC m f</kbd>    | Go to the next goal, if any.
+<kbd>SPC m ?</kbd>    | Show all goals.
+<kbd>SPC m e</kbd>    | Show the context of the goal at point.
+<kbd>SPC m b</kbd>    | Go to the previous goal, if any.
+<kbd>SPC m ,</kbd>    | Shows the type of the goal at point and the currect context.
+<kbd>SPC m =</kbd>    | Show constraints.
+<kbd>SPC m h</kbd>    | Compute the type of a hypothetical helper function.
+<kbd>SPC m d</kbd>    | Infers the type of the given expression.
+<kbd>SPC m w</kbd>    | Explains why a given name is in scope.
+<kbd>SPC m .</kbd>    | Shows the context, the goal and the given expression's inferred type.
+<kbd>SPC m o</kbd>    | Shows all the top-level names in the given module.
+<kbd>SPC m n</kbd>    | Computes the normal form of the given expression, using the scope of the current goal or, if point is not in a goal, the top-level scope.
+
+
+[Agda]: http://wiki.portal.chalmers.se/agda/pmwiki.php
diff --git a/contrib/lang/agda/extensions.el b/contrib/lang/agda/extensions.el
new file mode 100644
index 000000000..5b53556c6
--- /dev/null
+++ b/contrib/lang/agda/extensions.el
@@ -0,0 +1,48 @@
+;;; extensions.el --- Agda2 Layer extensions File for Spacemacs
+;;
+;; Copyright (c) 2012-2014 Sylvain Benner
+;; Copyright (c) 2015 Oliver Charles & Contributors
+;;
+;; Author: Oliver Charles <ollie@ocharles.org.uk>
+;; URL: https://github.com/syl20bnr/spacemacs
+;;
+;; This file is not part of GNU Emacs.
+;;
+;;; License: GPLv3
+
+(defvar agda-pre-extensions '(agda))
+
+(defun agda/init-agda ()
+  (custom-set-faces
+   '(agda2-highlight-datatype-face ((t (:inherit font-lock-type-face))))
+   '(agda2-highlight-function-face ((t (:inherit font-lock-type-face))))
+   '(agda2-highlight-inductive-constructor-face ((t (:inherit font-lock-function-name-face))))
+   '(agda2-highlight-keyword-face ((t (:inherit font-lock-keyword-face))))
+   '(agda2-highlight-module-face ((t (:inherit font-lock-constant-face))))
+   '(agda2-highlight-number-face ((t nil)))
+   '(agda2-highlight-postulate-face ((t (:inherit font-lock-type-face))))
+   '(agda2-highlight-primitive-type-face ((t (:inherit font-lock-type-face))))
+   '(agda2-highlight-record-face ((t (:inherit font-lock-type-face)))))
+
+  (load-file (let ((coding-system-for-read 'utf-8))
+               (shell-command-to-string "agda-mode locate")))
+
+  (evil-leader/set-key-for-mode 'agda2-mode
+    "ml" 'agda2-load
+    "ma" 'agda2-auto
+    "mr" 'agda2-refine
+    "ms" 'agda2-solveAll
+    "mt" 'agda2-goal-type
+    "mc" 'agda2-make-case
+    "mf" 'agda2-next-goal
+    "m?" 'agda2-show-goals
+    "me" 'agda2-show-context
+    "mb" 'agda2-previous-goal
+    "m," 'agda2-goal-and-context
+    "m=" 'agda2-show-constraints
+    "mh" 'agda2-helper-function-type
+    "md" 'agda2-infer-type-maybe-toplevel
+    "mw" 'agda2-why-in-scope-maybe-toplevel
+    "m." 'agda2-goal-and-context-and-inferred
+    "mo" 'agda2-module-contents-maybe-toplevel
+    "mn" 'agda2-compute-normalised-maybe-toplevel))