diff --git a/thesis/Justfile b/thesis/Justfile
deleted file mode 100644
index bae19e6..0000000
--- a/thesis/Justfile
+++ /dev/null
@@ -1,49 +0,0 @@
-set export
-builddir := `pwd` / "_build"
-
-all: gerby_db
-
-serve: gerby_db
-  #!/usr/bin/env bash
-  cd $builddir/gerby-website/gerby
-  cp tools/*.sqlite .
-  flask --app . run --host 0.0.0.0
-
-pdf: book_tex
-  tectonic $builddir/book.tex
-
-gerby_src:
-  #!/usr/bin/env bash
-  mkdir -p $builddir
-  if [ ! -d "$builddir/gerby-website" ]; then
-    git clone https://github.com/gerby-project/gerby-website $builddir/gerby-website
-  fi
-
-gerby_db: plastex_files gerby_src
-  #!/usr/bin/env bash
-  cd $builddir/gerby-website/gerby/tools
-  rm -rf stacks stacks.paux stacks.tags
-  cp -r $builddir/web/book stacks
-  cp $builddir/web/book.paux stacks.paux
-  cp $builddir/web/tags stacks.tags
-  python3 update.py
-
-plastex_files: book_tex tags bib
-  #!/usr/bin/env bash
-  mkdir -p $builddir/web
-  cd $builddir/web
-  rm -r book
-  cp tags $builddir/web/tags
-  cp $builddir/my.bib $builddir/web/my.bib
-  plastex --renderer=Gerby $builddir/book.tex
-
-tags:
-  mkdir -p $builddir
-  python3 scripts/update_tags.py tags
-
-bib:
-  touch $builddir/my.bib
-
-book_tex:
-  mkdir -p $builddir
-  python3 scripts/build_book.py > $builddir/book.tex
diff --git a/thesis/index b/thesis/index
deleted file mode 100644
index 0af535a..0000000
--- a/thesis/index
+++ /dev/null
@@ -1,4 +0,0 @@
-# Ordered index of modules
-
-src/intro.tex
-src/mltt.tex
diff --git a/thesis/preamble.tex b/thesis/preamble.tex
deleted file mode 100644
index 89274d8..0000000
--- a/thesis/preamble.tex
+++ /dev/null
@@ -1,3 +0,0 @@
-\documentclass{amsart}
-
-\usepackage{hyperref}
diff --git a/thesis/scripts/build_book.py b/thesis/scripts/build_book.py
deleted file mode 100644
index 0004c15..0000000
--- a/thesis/scripts/build_book.py
+++ /dev/null
@@ -1,65 +0,0 @@
-import os
-import sys
-from pathlib import Path
-
-def debug(*args, **kwargs): print(*args, file=sys.stderr, **kwargs)
-def is_label(t: str): return t.find("\\label{") >= 0
-
-with open("preamble.tex") as f:
-  for line in f.readlines():
-    line = line.strip()
-    if line.find("\\documentclass") == 0:
-      line = line.replace("amsart", "amsbook")
-      line = line.replace("stacks-project", "stacks-project-book")
-    print(line)
-
-print("""
-\\begin{document}
-
-\\begin{titlepage}
-\\pagestyle{empty}
-\\setcounter{page}{1}
-\\vskip1in
-\\noindent
-\\end{titlepage}
-""")
-
-ignored_lines = [
-  "\\input{preamble}",
-  "\\begin{document}",
-  "\\bibliography",
-  "\\end{document}",
-  "\\tableofcontents",
-  "\\input{chapters}",
-  "\\maketitle",
-]
-
-with open("index") as f:
-  files = []
-  for line in f.readlines():
-    line = line.strip()
-    if line.startswith("#"): continue
-    if line == "": continue
-    files.append(line)
-
-for fname in files:
-  file = Path(fname)
-  with open(file) as f:
-    print(f"\\part{{{file.stem}}}")
-    print(f"\\label{{{file.stem}}}")
-
-    for line in f.readlines():
-      line = line.strip()
-      if any(line.find(i) == 0 for i in ignored_lines):
-        continue
-      if is_label(line):
-        line = line.replace("\\label{", f"\\label{{{file.stem}-")
-      if line.find("\\title{") == 0:
-        line = line.replace("\\title{", "\\chapter{")
-      print(line)
-
-print("""
-\\bibliography{my}
-\\bibliographystyle{amsalpha}
-\\end{document}
-""")
diff --git a/thesis/scripts/update_tags.py b/thesis/scripts/update_tags.py
deleted file mode 100644
index 2a3b293..0000000
--- a/thesis/scripts/update_tags.py
+++ /dev/null
@@ -1,82 +0,0 @@
-import sys
-import click
-import pathlib
-import json
-import math
-import re
-
-letters = "0123456789ABCDEFGHJKLMNPQRSTUVWXYZ"
-label_pat = re.compile(r"\\label\{([^\}]*)\}")
-
-def tag2num(tag: str):
-  arr = [letters.find(c) for c in tag]
-  return sum(n * pow(len(letters), i) for i, n in enumerate(arr[::-1]))
-
-def num2tag(n: int):
-  largest = math.ceil(math.log(n, len(letters)))
-  coeffs = []
-  start = False
-  for i in range(largest, -1, -1):
-    p = pow(len(letters), i)
-    coeff, r = n // p, n % p
-    n = r
-    if coeff != 0:
-      start = True
-      coeffs.append(coeff)
-    elif start: coeffs.append(coeff)
-  return "".join(letters[c] for c in coeffs).zfill(4)
-
-def next_tag(nums: list[int], highest: int) -> tuple[int, int]:
-  prev = 0
-  for c in nums:
-    if c - prev > 1: return (prev + 1, highest)
-    prev = c
-  highest = min(prev, highest)
-  highest += 1
-  return (highest, highest)
-
-@click.command()
-@click.argument("filename", type=click.Path(path_type=pathlib.Path))
-def main(filename):
-  # Load existing tags
-  tag_numbers = []
-  tag_names = set()
-  try:
-    with open(filename) as f:
-      for line in f.readlines():
-        if line.startswith("#"): continue
-        tag_s, name = line.strip().split(",")
-        tag_n = tag2num(tag_s)
-        tag_numbers.append(tag_n)
-        tag_names.add(name)
-  except: pass
-
-  tag_numbers.sort()
-  highest_tag = tag_numbers[-1] if len(tag_numbers) > 0 else 0
-
-  new_tags = []
-  src_dir = pathlib.Path("src")
-  for file in src_dir.iterdir():
-    name = file.stem
-    with open(file) as f:
-      for line in f.readlines():
-        m = label_pat.match(line)
-        if m is None: continue
-        label = m.group(1)
-        full = f"{name}-{label}"
-        if full not in tag_names:
-          n, highest_tag = next_tag(tag_numbers, highest_tag)
-          tag_numbers.append(n)
-          if highest_tag != n: tag_numbers.sort()
-          new_tags.append((n, full))
-
-  # Write back to file
-  with open(filename, "a") as f:
-    for tag_n, name in new_tags:
-      tag_s = num2tag(tag_n)
-      f.write(f"{tag_s},{name}\n")
-    
-
-
-if __name__ == "__main__":
-  main()
diff --git a/thesis/src/intro.tex b/thesis/src/intro.tex
deleted file mode 100644
index 990e142..0000000
--- a/thesis/src/intro.tex
+++ /dev/null
@@ -1,19 +0,0 @@
-\input{preamble}
-
-\begin{document}
-
-\title{Introduction}
-
-\maketitle
-
-\phantomsection
-\label{section-phantom}
-
-\tableofcontents
-
-Hello
-
-
-
-\end{document}
-
diff --git a/thesis/src/mltt.tex b/thesis/src/mltt.tex
deleted file mode 100644
index 028b945..0000000
--- a/thesis/src/mltt.tex
+++ /dev/null
@@ -1,21 +0,0 @@
-\input{preamble}
-
-\begin{document}
-
-\title{Martin-Lof Type Theory}
-
-\maketitle
-
-\phantomsection
-\label{section-phantom}
-
-\tableofcontents
-
-\label{intro}
-
-
-\label{constructors-and-eliminators}
-
-
-
-\end{document}
diff --git a/thesis/style.typ b/thesis/style.typ
index 1e03d28..f7c2fac 100644
--- a/thesis/style.typ
+++ b/thesis/style.typ
@@ -20,7 +20,7 @@
   )
 
   show: thmrules
-  show link: body => underline(text(fill: olive, body))
+  show link: body => underline(text(fill: rgb("#009900"), body))
 
   // show heading: set block(above: 1.4em, below: 1em)
 
@@ -64,7 +64,8 @@
 #let eqv(a, b) = $#a tilde.eq #b$
 #let defEq(a, b) = $#a := #b$
 #let judgEqTyp(G, a, b, A) = $#G tack.r isTyp(#a equiv #b, #A)$
-#let imOf(f) = $sans("Im")(#f)$
+#let imSym = link(<image>)[$sans("Im")$]
+#let imOf(f) = $#imSym thin (f)$
 #let kerOf(f) = $sans("Ker")(#f)$
 #let ind = $sans("ind")$
 #let ap = $sans("ap")$
diff --git a/thesis/tags b/thesis/tags
deleted file mode 100644
index 57aac1e..0000000
--- a/thesis/tags
+++ /dev/null
@@ -1,4 +0,0 @@
-0001,mltt-section-phantom
-0002,mltt-intro
-0003,mltt-constructors-and-eliminators
-0004,intro-section-phantom