From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Sat, 10 Feb 2018 16:40:24 +0000 (-0500)
Subject: clarify PathP vs Path
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=84053d1c023721706ac5cbecf152e2cc71080518;p=cubicaltt.git

clarify PathP vs Path
---

diff --git a/lectures/lecture1.ctt b/lectures/lecture1.ctt
index 5226af9..27118ac 100644
--- 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
 
 {-