From 03b789ede04b6353156a39c4e2cbbe95135a1020 Mon Sep 17 00:00:00 2001
From: Philip Wadler <wadler@inf.ed.ac.uk>
Date: Wed, 19 Jul 2017 13:14:08 +0100
Subject: [PATCH] changes to README and index

---
 README.md | 23 +++++++++++++++++++----
 index.md  | 15 +++++++++++++++
 2 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index f47fe6e5..42f4e6a0 100644
--- a/README.md
+++ b/README.md
@@ -4,7 +4,22 @@ title: About
 permalink: /about/
 ---
 
-How to host literal code.
+This is a rewrite of the text
+
+* [Software Foundations](
+  https://softwarefoundations.cis.upenn.edu/current/index.html
+  )
+
+from Coq to Agda. The authors are
+
+* [Wen Kokke](
+  https://github.com/wenkokke
+  )
+* [Philip Wadler](
+  http://homepages.inf.ed.ac.uk/wadler/
+  )
+
+== How to host literal code
 
 In directory `sf/` the following:
 
@@ -20,13 +35,13 @@ For markdown commands see [Daring Fireball](
 https://daringfireball.net/projects/markdown/syntax
 ).
 
-Important git commands:
+== Important git commands:
 
     git pull
     git commit -am "message"
     git push
 
-[Unicode abbreviations](
+== [Unicode abbreviations](
 https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194
 ).
 
@@ -37,7 +52,7 @@ https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194
 	x\_1   x₁
 	x\_i   xᵢ
 
-Bindings for [Agda mode](
+== Bindings for [Agda mode](
 http://agda.readthedocs.io/en/latest/tools/emacs-mode.html
 )
 
diff --git a/index.md b/index.md
index 28d9da5c..807f0ff3 100644
--- a/index.md
+++ b/index.md
@@ -3,6 +3,21 @@ title  : Table of Contents
 layout : page
 ---
  
+This is a rewrite of the text
+
+* [Software Foundations](
+  https://softwarefoundations.cis.upenn.edu/current/index.html
+  )
+
+from Coq to Agda. The authors are
+
+* [Wen Kokke](
+  https://github.com/wenkokke
+  )
+* [Philip Wadler](
+  http://homepages.inf.ed.ac.uk/wadler/
+  )
+
 <!--
   - [Basics: Functional Programming in Agda]({{ "/Basics" | relative_url }})
 -->