diff --git a/index.md b/index.md
index 65cf767f..fb1c395b 100644
--- a/index.md
+++ b/index.md
@@ -18,38 +18,38 @@ fixes are encouraged.
 
 ## Front matter
 
-  - [Preface]({{ site.baseurl }}{% link out/Preface.md %})
+  - [Preface]({{ site.baseurl }}{% link out/plta/Preface.md %})
 
 ## Part 1: Logical Foundations
 
 (This part is ready for review. Please comment!)
 
-  - [Naturals: Natural numbers]({{ site.baseurl }}{% link out/Naturals.md %})
+  - [Naturals: Natural numbers]({{ site.baseurl }}{% link out/plta/Naturals.md %})
   - [Properties: Proof by induction](Properties)
-  - [Relations: Inductive definition of relations]({{ site.baseurl }}{% link out/Relations.md %})
-  - [Equality: Equality and equational reasoning]({{ site.baseurl }}{% link out/Equality.md %})
-  - [Isomorphism: Isomorphism and embedding]({{ site.baseurl }}{% link out/Isomorphism.md %})
-  - [Connectives: Conjunction, disjunction, and implication]({{ site.baseurl }}{% link out/Connectives.md %})
-  - [Negation: Negation, with intuitionistic and classical Logic]({{ site.baseurl }}{% link out/Negation.md %})
-  - [Quantifiers: Universals and existentials]({{ site.baseurl }}{% link out/Quantifiers.md %})
-  - [Lists: Lists and higher-order functions]({{ site.baseurl }}{% link out/Lists.md %})
-  - [Decidable: Booleans and decision procedures]({{ site.baseurl }}{% link out/Decidable.md %})
+  - [Relations: Inductive definition of relations]({{ site.baseurl }}{% link out/plta/Relations.md %})
+  - [Equality: Equality and equational reasoning]({{ site.baseurl }}{% link out/plta/Equality.md %})
+  - [Isomorphism: Isomorphism and embedding]({{ site.baseurl }}{% link out/plta/Isomorphism.md %})
+  - [Connectives: Conjunction, disjunction, and implication]({{ site.baseurl }}{% link out/plta/Connectives.md %})
+  - [Negation: Negation, with intuitionistic and classical Logic]({{ site.baseurl }}{% link out/plta/Negation.md %})
+  - [Quantifiers: Universals and existentials]({{ site.baseurl }}{% link out/plta/Quantifiers.md %})
+  - [Lists: Lists and higher-order functions]({{ site.baseurl }}{% link out/plta/Lists.md %})
+  - [Decidable: Booleans and decision procedures]({{ site.baseurl }}{% link out/plta/Decidable.md %})
 
 ## Part 2: Programming Language Foundations
 
 (This part is not yet ready for review.)
 
-  - [Lambda: Lambda: Introduction to Lambda Calculus]({{ site.baseurl }}{% link out/Lambda.md %})
-  - [LambdaProp: Properties of Simply-Typed Lambda Calculus]({{ site.baseurl }}{% link out/LambdaProp.md %})
-  - [DeBruijn: Inherently typed De Bruijn representation]({{ site.baseurl }}{% link out/DeBruijn.md %})
-  - [Extensions: Extensions to simply-typed lambda calculus]({{ site.baseurl }}{% link out/Extensions.md %})
-  - [Inference: Bidirectional type inference]({{ site.baseurl }}{% link out/Inference.md %})
-  - [Untyped: Untyped lambda calculus with full normalisation]({{ site.baseurl }}{% link out/Untyped.md %})
+  - [Lambda: Lambda: Introduction to Lambda Calculus]({{ site.baseurl }}{% link out/plta/Lambda.md %})
+  - [LambdaProp: Properties of Simply-Typed Lambda Calculus]({{ site.baseurl }}{% link out/plta/LambdaProp.md %})
+  - [DeBruijn: Inherently typed De Bruijn representation]({{ site.baseurl }}{% link out/plta/DeBruijn.md %})
+  - [Extensions: Extensions to simply-typed lambda calculus]({{ site.baseurl }}{% link out/plta/Extensions.md %})
+  - [Inference: Bidirectional type inference]({{ site.baseurl }}{% link out/plta/Inference.md %})
+  - [Untyped: Untyped lambda calculus with full normalisation]({{ site.baseurl }}{% link out/plta/Untyped.md %})
 
 ## Backmatter
 
-  - [Acknowledgements]({{ site.baseurl }}{% link out/Acknowledgements.md %})
-  - [Fonts: Test page for fonts]({{ site.baseurl }}{% link out/Fonts.md %})
+  - [Acknowledgements]({{ site.baseurl }}{% link out/plta/Acknowledgements.md %})
+  - [Fonts: Test page for fonts]({{ site.baseurl }}{% link out/plta/Fonts.md %})
 
 [sf]: https://softwarefoundations.cis.upenn.edu/
 [wen]: https://github.com/wenkokke