How to think about comp in cubical type theory

Consider the definition:

--  a             d
--  ^             ^
--  |             |
--  |             |
--  b------------>c
comp3Paths (A : U)
(a b c d: A)
(b2a : Path A b a)
(b2c: Path A b c)
(c2d: Path A c d) : Path A a d =
<i> comp (<_> A) (b2c @ i)
[ (i = 0) -> b2a , (i = 1) -> c2d ]


How does this actually compute a path from a to d? As best as I can tell, it will have to flip b2a, compose this with b2c, and finally compose this with c2d? In particular, if cubicaltt was equipped with a "path composition operator" ∘, could I have written the above as c2d ∘ b2c ∘(<i> b2a @ -i)?

If that's wrong, then what is the correct way to think about what comp does in cubicalTT?

Disclaimer: I've never actually implemented any variation of cubical type theories and I am not an expert in cubical type theory. I write this answer according to my own intuition. I welcome corrections and complementaries.

How does this actually compute a path from a to d?

The comp operator creates a term that has the following properties (in your case, not the general case):

• Reduces to a when i equals 0
• Reduces to d when i equals 1

That's how the path was created -- you can run the term (that has the above reduction rules) against the typing rule of path lambdas (the <i> a thing) in your head.

There is no primitive path composition in cubical type theory. It exists only in the model (or you can say the 'mathematical intuition'). The path composition ∘ we're talking about in cubical type theory is defined via comp, and comp is a primitive operator. I personally think of comp as the eliminator of the 'system' structure -- I'm not sure if it's the right way to think about it, but it worked for me.

Here's a more formal and general description: comp takes an open cube of any dimension (without a lid, and is described using the 'system' structure and an extra term representing the bottom). This cube has to satisfy several properties, such as agreement on intersections (like the side faces have to share the same edge connecting them). Then, by providing this open shape, comp becomes a term that reduces like this: take the face as the system describes and return the proper side of the face.

In your case, the faces are b2a and c2d and the bottom face is b2c, and they agree obviously. That's why this application to comp type-checks. Then, the term satisfying the computational rules described above was created, and, as the body of a path, it satisfies the type Path A a d. That's just how it worked.

Edit: here's some extra mathematical intuition. Think about the world of types and terms in the HoTT-ish sense, where there are spaces, points, lines, squares, cubes, etc., and these shapes can change geometrically but not topologically. There is a fact about this world: if given a cube where all of its sides and its bottom are connected, then this cube is, in fact, filled. Then we make this theorem a primitive operator called filling, and by filling a shape we can take its lid. Maybe the cubical folks think the 'take lid' operator is more primitive than 'filling', so they built the 'take lid' operator into the type theory, but IIRC these two operations can encode each other. There's nothing to do with concatenating anything, they are just connected. Connected things are always connected (so I don't think it's a good idea to say that there exists an operator ∘ because it does nothing. In fact, comp does nothing too, but it is a good theorem to rely on (at least better than ∘)), and composition happens to be such a good operator to implement in the type theory. If you want to read more, you may wanna search about 'kan condition'.