Worked on the layout.

.gitignore

@@ -1,3 +1,2 @@
 _site/
 .sass-cache/
-out/

_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

_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>

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 }})

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_,