From 84053d1c023721706ac5cbecf152e2cc71080518 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Sat, 10 Feb 2018 11:40:24 -0500 Subject: [PATCH] clarify PathP vs Path --- lectures/lecture1.ctt | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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 {- -- 2.34.1