So I'm trying to learn cubical type theory (specifically to use cubical agda), and there's one point that feels like I almost grasp it but not quite, and that's what exactly PathP is. I think I have a sort of intuition, so I wanted to ask if it's valid.

So I'm trying to learn cubical type theory (specifically to use cubical agda), and there's one point that feels like I almost grasp it but not quite, and that's what exactly

`PathP`

is. I think I have a sort of intuition, so I wanted to ask if it's valid.Is the difference between

`p: I -> Type`

and

`PathP p (p i0) (p i1)`

analogous to the difference between

`B: A -> Type`

and

`Pi x. B x`

?I believe so. At least, it seems to be typed similarly.