Path types - Type Theory

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Giovanni Santiago

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?