diff --git a/.github/workflows/github-pages.yml b/.github/workflows/github-pages.yml
new file mode 100644
index 0000000..e401d2f
--- /dev/null
+++ b/.github/workflows/github-pages.yml
@@ -0,0 +1,29 @@
+name: GitHub Pages
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+
+jobs:
+  build:
+    name: Deploy
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - uses: cachix/install-nix-action@v15
+      - uses: cachix/cachix-action@v10
+        with:
+          name: wolverian-agda-template
+          authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+      - name: Build HTML
+        run: nix build --verbose --print-build-logs
+      - name: Copy HTML so the next step can read it
+        run: cp -vHR result html
+      - name: GitHub Pages
+        uses: crazy-max/ghaction-github-pages@v2.5.0
+        with:
+          build_dir: html
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..f7781f1
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+*.agdai
+/_build/
+/html/
\ No newline at end of file
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..8d334e1
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,55 @@
+SRC_DIR := src
+OUTPUT_DIR := html
+
+AGDA := agda
+AGDA_FLAGS := \
+	--html \
+	--html-highlight=auto \
+	--highlight-occurrences \
+	--html-dir=$(OUTPUT_DIR)
+
+PANDOC := pandoc
+PANDOC_FLAGS := \
+	--to=html5 \
+	--standalone \
+	--section-divs \
+	--katex \
+	--css=pandoc.css \
+	--css=style.css \
+	--include-in-header=header.html
+
+FONTS_SRC := $(wildcard fonts/*.otf)
+FONTS_DST := $(foreach font,$(FONTS_SRC),$(OUTPUT_DIR)/fonts/$(notdir $(font)))
+
+STYLES_SRC := $(wildcard styles/*.css)
+STYLES_DST := $(foreach style,$(STYLES_SRC),$(OUTPUT_DIR)/$(notdir $(style)))
+
+.PHONY: all
+all: \
+	$(OUTPUT_DIR)/index.html \
+	$(OUTPUT_DIR)/header.html \
+	$(OUTPUT_DIR)/UCC.html \
+	$(STYLES_DST) \
+	$(FONTS_DST)
+
+$(OUTPUT_DIR)/%.md: $(SRC_DIR)/%.lagda.md
+	$(AGDA) $(AGDA_FLAGS) $<
+
+$(OUTPUT_DIR)/%.html: $(OUTPUT_DIR)/%.md $(STYLES_DST) $(FONTS_DST)
+	$(PANDOC) $(PANDOC_FLAGS) -o $@ $<
+
+$(OUTPUT_DIR)/fonts/%.otf: fonts/%.otf
+	@mkdir -p $(OUTPUT_DIR)/fonts
+	cp $< $@
+
+$(OUTPUT_DIR)/%.css: styles/%.css
+	@mkdir -p $(OUTPUT_DIR)
+	cp $< $@
+
+$(OUTPUT_DIR)/header.html: header.html
+	@mkdir -p $(OUTPUT_DIR)
+	cp $< $@
+
+$(OUTPUT_DIR)/index.html: index.md
+	@mkdir -p $(OUTPUT_DIR)
+	$(PANDOC) $(PANDOC_FLAGS) -o $@ $<
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..ac05b96
--- /dev/null
+++ b/README.md
@@ -0,0 +1,29 @@
+# Agda template
+
+## Prerequisites
+
+- Nix
+
+or
+
+- GNU `make`
+- Pandoc
+- Agda
+
+## Compile HTML
+
+Using Nix:
+
+```shellsession
+$ nix-build
+```
+
+Or, if you have the dependencies otherwise installed:
+
+```shellsession
+$ make all
+```
+
+## Continuous integration
+
+## License
diff --git a/agda-template.agda-lib b/agda-template.agda-lib
new file mode 100644
index 0000000..b05fc13
--- /dev/null
+++ b/agda-template.agda-lib
@@ -0,0 +1,2 @@
+depend: standard-library
+include: src
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..4646240
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,38 @@
+{
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let pkgs = nixpkgs.legacyPackages.${system};
+      in
+      rec {
+        defaultPackage = packages.wolverian-agda-template;
+        packages = {
+          wolverian-agda-template = pkgs.runCommand "wolverian-agda-template"
+            {
+              buildInputs = [
+                pkgs.gnumake
+                pkgs.pandoc
+                (pkgs.agda.withPackages (p: [ p.standard-library ]))
+              ];
+            }
+            ''
+              ln -s ${./fonts} fonts
+              ln -s ${./styles} styles
+              ln -s ${./index.md} index.md
+              ln -s ${./header.html} header.html
+              ln -s ${./Makefile} Makefile
+              ln -s ${./agda-template.agda-lib} agda-template.agda-lib
+              mkdir src && ln -s ${./src}/*.lagda.md src
+              ${pkgs.gnumake}/bin/make OUTPUT_DIR=$out
+            '';
+        };
+        checks = {
+          build = self.defaultPackage."${system}";
+        };
+      }
+    );
+}
diff --git a/fonts/LibertinusMath-Regular.otf b/fonts/LibertinusMath-Regular.otf
new file mode 100644
index 0000000..7be6151
Binary files /dev/null and b/fonts/LibertinusMath-Regular.otf differ
diff --git a/fonts/LibertinusSans-Bold.otf b/fonts/LibertinusSans-Bold.otf
new file mode 100644
index 0000000..478dbe3
Binary files /dev/null and b/fonts/LibertinusSans-Bold.otf differ
diff --git a/fonts/LibertinusSans-Italic.otf b/fonts/LibertinusSans-Italic.otf
new file mode 100644
index 0000000..fe2282c
Binary files /dev/null and b/fonts/LibertinusSans-Italic.otf differ
diff --git a/fonts/LibertinusSans-Regular.otf b/fonts/LibertinusSans-Regular.otf
new file mode 100644
index 0000000..e3cc0e8
Binary files /dev/null and b/fonts/LibertinusSans-Regular.otf differ
diff --git a/fonts/LibertinusSerif-Bold.otf b/fonts/LibertinusSerif-Bold.otf
new file mode 100644
index 0000000..3e78353
Binary files /dev/null and b/fonts/LibertinusSerif-Bold.otf differ
diff --git a/fonts/LibertinusSerif-BoldItalic.otf b/fonts/LibertinusSerif-BoldItalic.otf
new file mode 100644
index 0000000..a040174
Binary files /dev/null and b/fonts/LibertinusSerif-BoldItalic.otf differ
diff --git a/fonts/LibertinusSerif-Italic.otf b/fonts/LibertinusSerif-Italic.otf
new file mode 100644
index 0000000..7ed8bd8
Binary files /dev/null and b/fonts/LibertinusSerif-Italic.otf differ
diff --git a/fonts/LibertinusSerif-Regular.otf b/fonts/LibertinusSerif-Regular.otf
new file mode 100644
index 0000000..262c991
Binary files /dev/null and b/fonts/LibertinusSerif-Regular.otf differ
diff --git a/fonts/LibertinusSerif-Semibold.otf b/fonts/LibertinusSerif-Semibold.otf
new file mode 100644
index 0000000..8946b39
Binary files /dev/null and b/fonts/LibertinusSerif-Semibold.otf differ
diff --git a/fonts/LibertinusSerif-SemiboldItalic.otf b/fonts/LibertinusSerif-SemiboldItalic.otf
new file mode 100644
index 0000000..fdd8171
Binary files /dev/null and b/fonts/LibertinusSerif-SemiboldItalic.otf differ
diff --git a/fonts/LibertinusSerifDisplay-Regular.otf b/fonts/LibertinusSerifDisplay-Regular.otf
new file mode 100644
index 0000000..82c0da1
Binary files /dev/null and b/fonts/LibertinusSerifDisplay-Regular.otf differ
diff --git a/fonts/LibertinusSerifInitials-Regular.otf b/fonts/LibertinusSerifInitials-Regular.otf
new file mode 100644
index 0000000..d5f274e
Binary files /dev/null and b/fonts/LibertinusSerifInitials-Regular.otf differ
diff --git a/header.html b/header.html
new file mode 100644
index 0000000..b028655
--- /dev/null
+++ b/header.html
@@ -0,0 +1 @@
+<script src="highlight-hover.js"></script>
diff --git a/src/AgdaTemplate.lagda.md b/src/AgdaTemplate.lagda.md
new file mode 100644
index 0000000..5e5ac57
--- /dev/null
+++ b/src/AgdaTemplate.lagda.md
@@ -0,0 +1,5 @@
+# Agda template
+
+```
+data Example : Set where
+    Ok : Example
diff --git a/styles/pandoc.css b/styles/pandoc.css
new file mode 100644
index 0000000..e04f19b
--- /dev/null
+++ b/styles/pandoc.css
@@ -0,0 +1,164 @@
+html {
+  line-height: 1.5;
+  font-family: Georgia, serif;
+  font-size: 20px;
+  color: #1a1a1a;
+  background-color: #fdfdfd;
+}
+body {
+  margin: 0 auto;
+  max-width: 36em;
+  padding-left: 50px;
+  padding-right: 50px;
+  padding-top: 50px;
+  padding-bottom: 50px;
+  hyphens: auto;
+  overflow-wrap: break-word;
+  text-rendering: optimizeLegibility;
+  font-kerning: normal;
+}
+@media (max-width: 600px) {
+  body {
+    font-size: 0.9em;
+    padding: 1em;
+  }
+}
+@media print {
+  body {
+    background-color: transparent;
+    color: black;
+    font-size: 12pt;
+  }
+  p,
+  h2,
+  h3 {
+    orphans: 3;
+    widows: 3;
+  }
+  h2,
+  h3,
+  h4 {
+    page-break-after: avoid;
+  }
+}
+p {
+  margin: 1em 0;
+}
+a {
+  color: #1a1a1a;
+}
+a:visited {
+  color: #1a1a1a;
+}
+img {
+  max-width: 100%;
+}
+h1,
+h2,
+h3,
+h4,
+h5,
+h6 {
+  margin-top: 1.4em;
+}
+h5,
+h6 {
+  font-size: 1em;
+  font-style: italic;
+}
+h6 {
+  font-weight: normal;
+}
+ol,
+ul {
+  padding-left: 1.7em;
+  margin-top: 1em;
+}
+li > ol,
+li > ul {
+  margin-top: 0;
+}
+blockquote {
+  margin: 1em 0 1em 1.7em;
+  padding-left: 1em;
+  border-left: 2px solid #e6e6e6;
+  color: #606060;
+}
+code {
+  font-family: Menlo, Monaco, "Lucida Console", Consolas, monospace;
+  font-size: 85%;
+  margin: 0;
+}
+pre {
+  margin: 1em 0;
+  overflow: auto;
+}
+pre code {
+  padding: 0;
+  overflow: visible;
+  overflow-wrap: normal;
+}
+.sourceCode {
+  background-color: transparent;
+  overflow: visible;
+}
+hr {
+  background-color: #1a1a1a;
+  border: none;
+  height: 1px;
+  margin: 1em 0;
+}
+table {
+  margin: 1em 0;
+  border-collapse: collapse;
+  width: 100%;
+  overflow-x: auto;
+  display: block;
+  font-variant-numeric: lining-nums tabular-nums;
+}
+table caption {
+  margin-bottom: 0.75em;
+}
+tbody {
+  margin-top: 0.5em;
+  border-top: 1px solid #1a1a1a;
+  border-bottom: 1px solid #1a1a1a;
+}
+th {
+  border-top: 1px solid #1a1a1a;
+  padding: 0.25em 0.5em 0.25em 0.5em;
+}
+td {
+  padding: 0.125em 0.5em 0.25em 0.5em;
+}
+header {
+  margin-bottom: 4em;
+  text-align: center;
+}
+#TOC li {
+  list-style: none;
+}
+#TOC a:not(:hover) {
+  text-decoration: none;
+}
+code {
+  white-space: pre-wrap;
+}
+span.smallcaps {
+  font-variant: small-caps;
+}
+span.underline {
+  text-decoration: underline;
+}
+div.column {
+  display: inline-block;
+  vertical-align: top;
+  width: 50%;
+}
+div.hanging-indent {
+  margin-left: 1.5em;
+  text-indent: -1.5em;
+}
+ul.task-list {
+  list-style: none;
+}
diff --git a/styles/style.css b/styles/style.css
new file mode 100644
index 0000000..8842dd1
--- /dev/null
+++ b/styles/style.css
@@ -0,0 +1,143 @@
+html {
+  line-height: 1.15;
+  font-size: 80%;
+  font-family: Libertinus Serif, Georgia, serif;
+}
+body {
+  font-size: 1.8em;
+  line-height: 1.76;
+  max-width: none;
+}
+h1,
+h2,
+h3,
+h4,
+h5,
+h6 {
+  font-family: Libertinus Sans, system-ui, sans-serif;
+  letter-spacing: -1px;
+}
+h1 {
+  font-size: 3rem;
+}
+h2 {
+  font-size: 2.4rem;
+}
+h3 {
+  font-size: 2rem;
+}
+pre {
+  font-family: Libertinus Math, Georgia, serif;
+}
+pre a,
+code a {
+  text-decoration: none;
+}
+pre .hover-highlight,
+pre a:link:hover,
+code a:link:hover {
+  background-color: rgb(255, 255, 145) !important;
+}
+
+/* KaTeX Overrides */
+
+header,
+.katex-display,
+.katex-display > .katex {
+  text-align: inherit !important;
+}
+.katex,
+.katex .mathdefault {
+  font-family: Libertinus Math, KaTeX_Main, Georgia, serif !important;
+  font-size: 1em !important;
+}
+
+/* Font Faces */
+
+/* Sans Regular */
+@font-face {
+  font-family: "Libertinus Sans";
+  src: url(fonts/LibertinusSans-Regular.otf);
+  font-weight: 400;
+  font-style: normal;
+}
+
+/* Sans Italic */
+@font-face {
+  font-family: "Libertinus Sans";
+  src: url(fonts/LibertinusSans-Italic.otf);
+  font-weight: 400;
+  font-style: italic;
+}
+
+/* Sans Bold */
+@font-face {
+  font-family: "Libertinus Sans";
+  src: url(fonts/LibertinusSans-Bold.otf);
+  font-weight: 700;
+  font-style: normal;
+}
+
+/* Regular */
+@font-face {
+  font-family: "Libertinus Serif";
+  src: url(fonts/LibertinusSerif-Regular.otf);
+  font-weight: 400;
+  font-style: normal;
+}
+
+/* Semibold */
+@font-face {
+  font-family: "Libertinus Serif";
+  src: url(fonts/LibertinusSerif-Semibold.otf);
+  font-weight: 600;
+  font-style: normal;
+}
+
+/* Bold */
+@font-face {
+  font-family: "Libertinus Serif";
+  src: url(fonts/LibertinusSerif-Bold.otf);
+  font-weight: 700;
+  font-style: normal;
+}
+
+/* Regular Italic */
+@font-face {
+  font-family: "Libertinus Serif";
+  src: url(fonts/LibertinusSerif-Italic.otf);
+  font-weight: 400;
+  font-style: italic;
+}
+
+/* Semibold Italic */
+@font-face {
+  font-family: "Libertinus Serif";
+  src: url(fonts/LibertinusSerif-SemiboldItalic.otf);
+  font-weight: 600;
+  font-style: italic;
+}
+
+/* Bold Italic */
+@font-face {
+  font-family: "Libertinus Serif";
+  src: url(fonts/LibertinusSerif-BoldItalic.otf);
+  font-weight: 700;
+  font-style: italic;
+}
+
+/* Math */
+@font-face {
+  font-family: "Libertinus Math";
+  src: url(fonts/LibertinusMath-Regular.otf);
+  font-weight: 400;
+  font-style: normal;
+}
+
+/* Display */
+@font-face {
+  font-family: "Libertinus Display";
+  src: url(fonts/LibertinusSerifDisplay-Regular.otf);
+  font-weight: 400;
+  font-style: normal;
+}