update lectures

diff --git a/lectures/lecture1.ctt b/lectures/lecture1.ctt
index 9366c861088d3639bbb028c51f4093c8e897af8d..5226af9d4010942c54ab0a7a0085b4722d0de3a8 100644 (file)
--- a/lectures/lecture1.ctt
+++ b/lectures/lecture1.ctt
@@ -261,6 +261,13 @@ or : bool -> bool -> bool = split
 -- appear in the rest of the term (in particular one cannot refer to a
 -- variable called _).
 
+-- Note also that the syntax is indentation sensitive (like in
+-- Haskell), so the following does not parse:
+--
+-- foo : bool = let output : bool =
+--                  true
+--              in output
+
 -- Sigma types are built-in and written as (x : A) * B:
 Sigma (A : U) (B : A -> U) : U = (x : A) * B x
 
@@ -491,7 +498,7 @@ That's all for the first lecture. Next time we will look at:
   elimination principle for Path types. In particular how to prove
   transitivity of path types:
 
-  trans (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c =
+  compPath (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c =
 
   and that we can substitute Path equal elements:
 

diff --git a/lectures/lecture2.ctt b/lectures/lecture2.ctt
index 13e0570873304008ded784656caacf4d2dc4fb7e..73e489024b67f0a3fb3efd6a33d134dd940fd812 100644 (file)
--- a/lectures/lecture2.ctt
+++ b/lectures/lecture2.ctt
@@ -242,7 +242,7 @@ writing the comp after a path-abstraction). The direction j that we
 are doing the composition in is implicit, more about this below.
 
 -}
-trans (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c =
+compPath (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c =
   <i> comp (<_> A) (p @ i)
                    [ (i = 0) -> <j> a
                    , (i = 1) -> q ]