lecture1

diff --git a/lectures/lecture1.ctt b/lectures/lecture1.ctt
index 4bb11627e36b8183ac3d2ddadda0d3dd285cdb3e..9e16c9d47852e1be2d96c4c99dcc499995c777fa 100644 (file)
--- a/lectures/lecture1.ctt
+++ b/lectures/lecture1.ctt
@@ -141,7 +141,8 @@ model:
 to nominal sets with 01 substitutions:
 
   "An Equivalent Presentation of the Bezem-Coquand-Huber Category of
-  Cubical Sets" by Andrew Pitts.
+  Cubical Sets"
+  Andrew Pitts
   https://arxiv.org/abs/1401.7807
 
 Before implementing cubicaltt (so in 2013-2014) we implemented a
@@ -198,6 +199,9 @@ idfun : (A : U) (a : A) -> A =
 -- Or even better like this:
 idfun (A : U) (a : A) : A = a
 
+-- The syntax for Pi types is like in Agda, so (x : A) -> B
+-- corresponds to Pi (x : A). B or forall (x : A), B.
+
 -- Note that the second idfun shadows the first, so when one uses
 -- idfun later this will refer to the last defined one.
 -- TODO: This is a little dangerous if one have a long development and
@@ -422,8 +426,8 @@ congbin (A B C : U) (f : A -> B -> C) (a a' : A) (b b' : B)
 -- type. We could have a version of undefined which is annotated with
 -- the type (similar to what we have for split), but this hasn't been
 -- implemented yet. Note that it is often useful to define a local
--- undefined definition using let-in or where and keep the body
--- undefined when trying to prove complicated things.
+-- definition using let-in or where and keep the body of it undefined
+-- when trying to prove complicated things.
 
 -- We get a short proof of function extensionality using Path types:
 funExt (A B : U) (f g : A -> B)
@@ -457,6 +461,9 @@ funExt2 (A B C : U) (f g : A -> B -> C)
 compf (f g : bool -> bool) : bool -> bool =
   \(b : bool) -> g (f b)
 
+-- WARNING: we couldn't have called the above function comp as comp is
+-- a reserved keyword.
+
 notK' : Path (bool -> bool) (compf not not) (idfun bool) =
   <i> \(b : bool) -> notK b @ i