awodey
diff --git a/‎.DS_Store
0 Bytes b/‎.DS_Store
0 Bytes
diff --git a/‎typetheory/.DS_Store
0 Bytes b/‎typetheory/.DS_Store
0 Bytes
diff --git a/‎typetheory/index.md
+1 b/‎typetheory/index.md
+1
diff --git a/‎typetheory/notes/index.md
+1 b/‎typetheory/notes/index.md
+1
diff --git a/‎typetheory/notes/typetheory3a.pdf
310 KB b/‎typetheory/notes/typetheory3a.pdf
310 KB
@@ -65,6 +65,7 @@ Watch this space for news and information!
 - Here are some other [notes on Kripke completeness of Simple Type Theory](/typetheory/notes/KripkeSTT.pdf).
 - Also check out the course notes from [Fischbachau](../fischbachau/) for a bigger picture.
 - the [lecture notes](/typetheory/notes/typetheory2.pdf) for simple type theory are now complete.
+- the first set of [lecture notes](/typetheory/notes/typetheory3a.pdf) for dependent type theory are now available.
 <!---
 - The [lecture notes](/catlog/notes/catlog1.pdf) for (the first half of) Chapter 1 on Algebraic Theories are available.  
 - The [lecture notes](/catlog/notes/catlog1.pdf) for Chapter 1 on Algebraic Theories are now complete. 
 
@@ -6,6 +6,7 @@ Lecture notes will accumulate here as the course proceeds.
 - [typetheory1.pdf](typetheory1.pdf)
 - Here are some other [notes on Kripke completeness of Simple Type Theory](KripkeSTT.pdf).
 - [typetheory2.pdf](typetheory2.pdf)
+- [typetheory3a.pdf](typetheory3a.pdf)
 <!--
 -->