diff --git a/.gitignore b/.gitignore
index 2819725..bc782f7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,3 +2,4 @@
 .agda-html
 _site
 *.agdai
+.jekyll-metadata
diff --git a/_layouts/default.html b/_layouts/default.html
index 7415c29..1d99d02 100644
--- a/_layouts/default.html
+++ b/_layouts/default.html
@@ -3,14 +3,17 @@
   <head>
     <meta name="viewport" content="width=device-width, initial-scale=1">
     <meta charset="utf-8">
+    <meta name="description" content="{{ page.title }}">
+    <meta name="author" content="Rachel Samuelsson">
     <title>{{ page.title }} - {{ site.title }}</title>
     <link rel="stylesheet" href="{{ "/assets/css/main.css" | relative_url }}">
+    <a hidden rel="me" href="https://types.pl/@rachelrosen">Mastodon</a>
   </head>
   <body>
     {{ content }}
   </body>
   <head>
     <link rel="stylesheet" href="{{ "/assets/css/katex.css" | relative_url }}">
-	  <link rel="stylesheet" href="{{ "/lagda/Agda.css" | relative_url }}">
+    <link rel="stylesheet" href="{{ "/lagda/Agda.css" | relative_url }}">
   </head>
 </html>
diff --git a/_layouts/nav.html b/_layouts/nav.html
index e10b7f1..7970656 100644
--- a/_layouts/nav.html
+++ b/_layouts/nav.html
@@ -7,6 +7,7 @@ layout: default
   </nav></ul>
   <hr>
   <nav><ul>
+    <li><a href="/work.html">work</a></li>
     <li><a href="/">blog</a></li>
     <li><a href="/about.html">about</a></li>
   </nav></ul>
diff --git a/work.html b/work.html
new file mode 100644
index 0000000..c967bad
--- /dev/null
+++ b/work.html
@@ -0,0 +1,37 @@
+---
+layout: other
+title: "work"
+---
+
+{% katexmm %}
+<h2>projects</h2>
+
+<h3>ongoing</h3>
+<ul>
+  <li><a href="">implicitt</a> - An implementation of a dependent type system with first class implicit pi types, metavariables, and holes.</li>
+  <li><a href="">this website</a> - The project which never ends.</li>
+</ul>
+
+<h3>completed</h3>
+<ul>
+  <li><a href="">pi</a> - An implementation of type-in-type MLTT, with pi, sigma, identity, and natural number types.
+  <li><a href="">hm</a> - An implementation of a Hindley-Milner type system with non-indexed inductive types. Strictly terminating, other than a hole in the positivity checker.</li>
+  <li><a href="">viddl</a> - A web front-end for youtube-dl</li>
+  <li><a href="">kino</a> - A TUI client for browsing movies</li>
+  <li><a href="">bc</a> - A brainfuck compiler, outputting ELF binaries for 64-bit linux.</li>
+  <li><a href="">mpdart</a> - An album art display for the music player mpd</li>
+  <li><a href="">dbg.h</a> - A C header using macros and C11 generics in order to create greatly informative debug messages.</li>
+</ul>
+
+<h3>put off</h3>
+<ul>
+  <li><a href="">cwfs</a> - A formalisation of categories with families in cubical agda. Put off due to the extensional nature of the theory making formalisation a pain. I plan to retry with natural models <em>sometime</em> in the future.</li>
+  <li><a href="">secd</a> - An implementation of a VM designed as a compilation target for languages based on the lambda calculus. Put off due to not wanting to work out implementation details or write more C. I hope to use what I learned for optimized evaluation of closures in a dependent type system some day.</li>
+</ul>
+
+<h2>teaching assistant work</h2>
+<table>
+  <tr><th>Role</th><th>Course</th><th>Duration</th></tr>
+  <tr><td>Teaching Assistant</td><td>TDA555 - Introduction to functional programming</td><td>2022-08-22 - 2022-11-04</td></tr>
+</table>
+{% endkatexmm %}
