diff --git a/modules/home/users/msyds/emacs/lisp/syd/agda.el b/modules/home/users/msyds/emacs/lisp/syd/agda.el
index 21ba724..c1240f5 100755
--- a/modules/home/users/msyds/emacs/lisp/syd/agda.el
+++ b/modules/home/users/msyds/emacs/lisp/syd/agda.el
@@ -11,6 +11,42 @@
       (format "%s locate" agda-mode-path))))
   (setq agda2-program-name (executable-find "agda")))
 
+(defface syd-agda2-default
+  `((t :font ,(font-spec :family "IBM Plex Sans" :size 17)
+       :height unspecified))
+  "Default face from which all agda2-* faces inherit.")
+
+(defvar syd-agda2-symbol-font
+  (font-spec :family "IBM Plex Math")
+  "Math font for Agda symbols.")
+
+(defvar syd-agda2-faces
+  ;; (let (faces)
+  ;;   (mapatoms (lambda (s)
+  ;; 		(if (and (facep s) (s-prefix? "agda2-" (symbol-name s)))
+  ;; 		    (push s faces))))
+  ;;   faces)
+  '(agda2-highlight-positivity-problem-face agda2-highlight-symbol-face
+    agda2-highlight-coverage-problem-face agda2-highlight-record-face
+    agda2-highlight-pragma-face agda2-highlight-inductive-constructor-face
+    agda2-highlight-instance-problem-face agda2-highlight-dotted-face
+    agda2-highlight-missing-definition-face agda2-highlight-deadcode-face
+    agda2-highlight-error-face agda2-highlight-function-face
+    agda2-highlight-string-face agda2-highlight-keyword-face
+    agda2-highlight-datatype-face agda2-highlight-postulate-face
+    agda2-highlight-primitive-type-face agda2-highlight-module-face
+    agda2-highlight-operator-face agda2-highlight-primitive-face
+    agda2-highlight-unsolved-constraint-face
+    agda2-highlight-generalizable-variable-face
+    agda2-highlight-catchall-clause-face agda2-highlight-field-face
+    agda2-highlight-shadowing-in-telescope-face
+    agda2-highlight-error-warning-face agda2-highlight-typechecks-face
+    agda2-highlight-termination-problem-face
+    agda2-highlight-confluence-problem-face agda2-highlight-macro-face
+    agda2-highlight-coinductive-constructor-face
+    agda2-highlight-bound-variable-face agda2-highlight-unsolved-meta-face
+    agda2-highlight-cosmetic-problem-face agda2-highlight-number-face))
+
 (with-eval-after-load 'agda2
   (general-define-key
    :keymaps 'agda2-mode-map
@@ -50,7 +86,7 @@
     ;; FUCLK!!!!!!!!!
     "g d" #'agda2-goto-definition-keyboard
     "K" #'agda2-goal-and-context)
-  (setq agda2-fontset-name "JuliaMono")
+  ;; (setq agda2-fontset-name "JuliaMono")
 
   (add-to-list
    'auto-mode-alist
@@ -83,4 +119,26 @@
   (syd-handle 'agda2-mode
     :docs #'syd-agda-lookup-documentation))
 
+(with-eval-after-load 'agda2-highlight
+  (set-face-attribute
+   'agda2-highlight-symbol-face nil
+   :family "IBM Plex Math")
+
+  (defvar syd-agda-init-info-buffer-hook)
+
+  (syd-defadvice syd-agda--run-agda-init-info-buffer-hook-a ()
+    :after #'agda2-info-buffer
+    (with-current-buffer agda2-info-buffer
+      (run-hooks 'syd-agda-init-info-buffer-hook)))
+
+  (syd-add-hook '(agda2-mode-hook syd-agda-init-info-buffer-hook)
+    (defun syd-agda--configure-fonts-h ()
+      (setq-local use-default-font-for-symbols nil)
+      (buffer-face-set 'syd-agda2-default)
+      (set-fontset-font
+       t 'symbol syd-agda2-symbol-font)
+      (face-remap-add-relative
+       'highlight
+       `((t :font ,(font-spec :family "IBM Plex Mono")))))))
+
 (provide 'syd/agda)