diff --git a/.gitignore b/.gitignore
index 54851a9c..0c3e5abb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,2 @@
 _site/
 .sass-cache/
-out/
diff --git a/_config.yml b/_config.yml
index c17b40fd..e42417b5 100644
--- a/_config.yml
+++ b/_config.yml
@@ -1,4 +1,5 @@
 title: Agda Software Foundations
+author: Pepijn Kokke
 email: pepijn.kokke@gmail.com
 description: > 
   Write an awesome description for your new site here. You can edit this
@@ -7,6 +8,8 @@ description: >
 baseurl: "/sf"
 url: "https://pepijnkokke.github.io"
 github_username: pepijnkokke 
+disqus:
+  shortname: pepijnkokke
 
 # Build settings
 markdown: kramdown
diff --git a/_includes/header.html b/_includes/header.html
new file mode 100644
index 00000000..bd35490d
--- /dev/null
+++ b/_includes/header.html
@@ -0,0 +1,24 @@
+<header class="site-header" role="banner">
+
+    <div class="wrapper">
+
+        <a class="site-title" href="{{ "/" | relative_url}}">{{ site.title | escape }}</a>
+
+        <nav class="site-nav">
+            <span class="menu-icon">
+                <svg viewBox="0 0 18 15" width="18px" height="15px">
+                    <path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
+                    <path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
+                    <path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
+                </svg>
+            </span>
+
+            <div class="trigger">
+                <a class="page-link" href="{{ "/" | relative_url }}">Table of Contents</a>
+                <a class="page-link" href="{{ "/about" | relative_url }}">About</a>
+            </div>
+        </nav>
+
+    </div>
+
+</header>
diff --git a/index.md b/index.md
index 1eb5d672..13e9d65a 100644
--- a/index.md
+++ b/index.md
@@ -1,6 +1,9 @@
 ---
-# You don't need to edit this file, it's empty on purpose.
-# Edit theme's home layout instead if you wanna make some changes
-# See: https://jekyllrb.com/docs/themes/#overriding-theme-defaults
-layout: home
+title  : Table of Contents
+layout : page
 ---
+ 
+  - [Basics: Functional Programming in Agda]({{ "/Basics" | relative_url }})
+  - [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }})
+  - [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }})
+  - [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }})
diff --git a/src/Stlc.lagda b/src/Stlc.lagda
index 29e4c6e3..fbb64e8f 100644
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@@ -19,7 +19,7 @@ open import Relation.Nullary using (Dec; yes; no)
 open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
 \end{code}
 
-# The Simply Typed Lambda-Calculus
+# Stlc: The Simply Typed Lambda-Calculus
 
 The simply typed lambda-calculus (STLC) is a tiny core
 calculus embodying the key concept of _functional abstraction_,