What should we return when pattern matching on a Path constructor?
it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer


My understanding is that it matches points of path rather than path itself. This is why the matching is on posneg x (where x : I) rather than posneg itself.

Since paths can be seen as (special) maps from I, we can think of HIT constructors as just a special of regular constructors, i.e.

  posneg : I ↝ HitInt [i0 ↦ pos 0 ; i1 ↦ neg 0]


where if you ignore "special" properties of Interval, it looks like a regular constructor (in cubicaltt notation it already looks similar except that I is always treated specially).


  What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.


It's the only way to satisfy constraints imposed by previous definitions (this works for both zero cases). In fact, Agda can correctly solve even two holes (in right order):

sucHitInt : HitInt → HitInt
sucHitInt (pos n) = pos (suc n)
sucHitInt (posneg i) = {!!}
sucHitInt (neg zero) = {!!}
sucHitInt (neg (suc n)) = neg n



  Why it's not returning a Path like  pos 1 (even this is not a member of the higher inductive family)?


Again, since we're matching on points rather than paths; for symmetry it's possible to imagine that case as equal to:

sucHitInt (posneg i) = (λ _ → pos 1) i


reading somewhat like "for all projections from I at i to path posneg we have projections from I at I to constant path (λ _ → pos 1)". This doesn't quite work in Agda (because typecheking lambda application directly isn't very well supported), however the following (with the same meaning) does:

sucHitInt (posneg i) = refl {x = pos 1} i


Finally, abusing notation, we could rewrite that as

(ap sucHitInt posneg) i = (refl {x = pos 1}) i


(where ap (from the HoTT book) corresponds to cong in typical Agda) and, getting rid of i from the both sides, recover path to path mapping.

PS: i'm new to cubical myself, so hopefully someone can correct or extend my answer