Judgemental equalities of path composition I have yet another question about Cubical Type Theory, this time involving path composition.
I think I have grasped the face systems and formation of the comp primitive. However, the way it reduces in particular cases is a big mystery to me.
In the following section, let A,X be types, p,q paths (their orientation should be clear from context), a,b,x,... points. Endpoints of the interval are 1i and 0i.
For example, does <i> comp (<_> A) (p @ i) [(i=0i) => <_> a, (i=1i) => <_> b] produce p?
What is the difference between <i> comp X (p @ i) [] and <i> comp X (p @ i) [(i=0i) => <_> a]? Is an omitted face bound the same as identity-path face bound?
How does one prove that <i> comp (<_> A) (p @ i) [(i=0i) => <_> a, (i=1i) => q] and comp (<i> Path A a (q @ i)) p [] are the same? Or are they?
Last but not least, does it matter which paths we use in the face bounds? I mean what is the difference between <i> comp (<_> A) (p @ i) [(i=0i) => <_> a, (i=1i) => q] and <i> comp (<_> A) b [(i=0i) => <j> p @ -j, (i=1i) => q]?
The corresponding cubes are:
a - - - - > c
^           ^
|           |
| <_> a     | q
|           |
|     p     |
a --------> b          (comp1)

a - - - - > c
^           ^
|           |
| inv p     | q
|           |
|   <_> b   |
b --------> b          (comp2)

I think they ought to be equal, but how does one derive such a judgement?
 A: I'm not the most expert in this stuff (I learned some stuff writing this up); more someone who fools around with an implementation (cubical Agda) and reading papers. As an aside, do you have an actual implementation to fool around with? Some of these questions can be answered by actually trying them out.

For example, does <i> comp (<_> A) (p @ i) [(i=0i) => <_> a, (i=1i) => <_> b] produce p?

No (hcomp is a homogeneous version of comp that is primitive in Agda, which is appropriate because your <_> A is constant):
hmm : (x y : A) (p : x ≡ y) → x ≡ y
hmm x y p i = hcomp (λ{ _ (i = i0) → x ; _ (i = i1) → y }) (p i)

hmmm : (x y : A) (p : x ≡ y) → p ≡ hmm x y p
hmmm x y p = refl -- this doesn't work

I think the important thing to keep in mind is that the 'system' (or whatever the face specification is called in what you're reading) specifies exactly the cases where comp reduces away (completely) due to dimensional refinements. So, in this case, when i = i0 it reduces to x and when i = i1 it reduces to y, and in between it does not reduce. And so:

What is the difference between <i> comp X (p @ i) [] and <i> comp X (p @ i) [(i=0i) => <_> a]? Is an omitted face bound the same as identity-path face bound?

If you omit all faces, the comp doesn't reduce away regardless of the choice of i. Incidentally, the type of hcomp in Agda is:
hcomp  : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A

Partial φ A is the type of the face system. φ tells you where hcomp reduces away. It does so when φ = i1. So you can write:
always : (x : A) → A
always x = hcomp {φ = i1} (λ _ _ → x) x

And this reduces to x. In order to give the empty system using a pattern, we need to write:
never : (x : A) → A
never x = hcomp {φ = i0} (λ _ ()) x

And this doesn't reduce further (λ _ () could be written λ _ → empty and the {φ = i0} could be omitted) unless we know something about x/A. Usually the specification of the system is enough to infer φ, I guess, so cubical Agda makes it an implicit argument.

How does one prove that <i> comp (<_> A) (p @ i) [(i=0i) => <_> a, (i=1i) => q] and comp (<i> Path A a (q @ i)) p [] are the same? Or are they?

module _ (x y z : A) (p : x ≡ y) (q : y ≡ z) where
  r : x ≡ z
  r i = hcomp (λ{ _ (i = i0) → x ; k (i = i1) → q k}) (p i)

  s : x ≡ z
  s = comp (λ i → Path A x (q i)) {φ = i0} (λ _ ()) p

comp with an empty face is actually one way of specifying another primitive operation in cubical Agda:
transp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) (φ : I) (a : A i0) → A i1

Homogeneous composition (hcomp) and moving around in a heterogeneous type (transp) are divided into separate 'simpler' operations, and comp is derived. So, in Agda, s reduces to:
-- the computer told me this
hcomp (λ i → empty) (transp (λ i → x ≡ q i) i0 p)

As an intermediate step, it will help me to define just the transp part, which has the same type:
  s' : x ≡ z
  s' = transp (λ i → x ≡ q i) i0 p

This can be proved equal to s by taking advantage of how φ/faces cause hcomp to reduce, and how systems themselves reduce. The proof is probably a good enough example:
  simpler : s ≡ s'
  simpler i = hcomp (λ{ _ (i = i1) → s'}) s'

So, when i = i1, this reduces to s', so the right side is valid. Because we haven't specified an i = i0 face, the hcomp doesn't reduce away at that end. But, the system gets refined to throw away contradictory cases, like (i0 = i1). So at the left end, the system reduces to the empty system, and we're left with the reduced term I gave for s.
Now, the final proof is going to involve knowing the last (I think) way that comp can reduce. If A is not simply an abstract type, then comp can reduce due to type-specific rules. The simplest example I can think of is this:
nat : ℕ
nat = hcomp {φ = i0} (λ{ _ () }) 1

canonical : nat ≡ 1
canonical = refl

So, even though hcomp with the empty system doesn't reduce in general, for concrete values it does reduce (this also means that for your first question, particular choices of p might cause the answer to be 'yes' instead). There are reduction rules for every type former commuting through (h)comp and transp, and this means that the following equation holds (the λ where syntax lets me write things with indentation instead of braces and semicolons):
  -- the computer almost told me this (it used a worse syntax)
  reduct : ∀ i → s' i ≡ hcomp (λ where
                                 k (i = i0) → transp (λ _ → A) k x
                                 k (i = i1) → transp (λ _ → A) k (q k))
                              (transp (λ _ → A) i0 (p i))
  reduct i = refl

Now, transp has similar reduction cases to comp, even though there's no system involved. Its second visible argument is φ, and it reduces away completely when φ = i1. The rule for choosing φ is that its first argument must be judgmentally constant when φ = i1. In the above case it's always constant, so we could pick whatever we want.
So, hopefully it's not too hard to see that s' i has actually reduced to r i with some extra transp noise thrown in. The way you get rid of that is similar to the above hcomp trick: you use transp with a φ such that it reduces at one end, and doesn't at the other. So for instance:
  reducti0 : x ≡ transp (λ _ → A) i0 x
  reducti0 i = transp (λ _ → A) (~ i) x

  reductik : ∀ k → transp (λ _ → A) k (q k) ≡ q k
  reductik k i = transp (λ _ → A) (k ∨ i) (q k)

So we can prove that r and s' are equivalent like so:
  complicated : r ≡ s'
  complicated j i
    = hcomp (λ where
        k (i = i0) → transp (λ _ → A) (k ∨ ~ j) x
        k (i = i1) → transp (λ _ → A) (k ∨ ~ j) (q k))
        (transp (λ _ → A) (~ j) (p i))

When j = i0, ~ j = k ∨ ~ j = i1 and all these transps disappear. When j = i1, ~ j = i0 and k ∨ ~ j = k, and the transp terms match s'.

Last but not least, does it matter which paths we use in the face bounds? I mean what is the difference between <i> comp (<_> A) (p @ i) [(i=0i) => <_> a, (i=1i) => q] and <i> comp (<_> A) b [(i=0i) => <j> p @ -j, (i=1i) => q]?

If you only care about the endpoints, it doesn't matter much. However, in the middle, they will not be judgmentally equal. So the choice will affect which higher equivalences are easier to prove and whatnot.
If you create the filled squares instead, then they will reduce to different things on different edges, so those will also be judgmentally different.
They can be proved equivalent by pulling things around corners and such, though.
  t : x ≡ z
  t i = hcomp (λ{ k (i = i0) → p (~ k) ; k (i = i1) → q k }) y

  mediate : r ≡ t
  mediate j i
    = hcomp (λ where
          k (i = i0) → p (~ k ∧ j)
          k (i = i1) → q k)
        (p (j ∨ i))

The exact details of all this are dependent on the primitives chosen. Agda has hcomp and transp as its primitive operations. Some papers I've seen use comp and derive those two as special cases. There's also Cartesian cubical type theory which has a somewhat different comp operation (and doesn't have ∧ and ∨). But all of them will have some way to get the results above, I think.
Again, though, I'd recommend getting an implementation of this and using it on a computer. It is the computer's job to manipulate the judgmental equalities for you, so you can ask it these questions and get much faster answers. And probably you can look at a much larger body of proofs to figure out the tricks necessary to do the proofs like your last two sorts of questions.
