clarify PathP vs Path

diff --git a/lectures/lecture1.ctt b/lectures/lecture1.ctt
index 5226af9d4010942c54ab0a7a0085b4722d0de3a8..27118aced04f667c16943c0d15f87679f761f8d2 100644 (file)
--- a/lectures/lecture1.ctt
+++ b/lectures/lecture1.ctt
@@ -351,9 +351,10 @@ where r is some element of the interval.
 -}
 
 
--- As in the Cubical Type Theory paper the type PathP (written Path in
--- the paper!) is heterogeneous. The homogeneous Path type can be
--- defined by:
+-- The type PathP is a heterogeneous path type and it corresponds to
+-- the Path type introduced in section 9.2 of the cubical type theory
+-- paper. The homogeneous Path type, corresponding to the one in
+-- section 3 of the paper, can then be defined by:
 Path (A : U) (a b : A) : U = PathP (<_> A) a b
 
 {-