From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Fri, 3 Nov 2017 03:00:54 +0000 (-0400)
Subject: update lectures
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=3d3e890963c6d90d3586e063dd4beba343b1481c;p=cubicaltt.git

update lectures
---

diff --git a/lectures/lecture1.ctt b/lectures/lecture1.ctt
index 9366c86..5226af9 100644
--- 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 13e0570..73e4890 100644
--- 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 ]