What should we return when pattern matching on a Higher Indutive Type and the case is a Path?

Question

Context: Cubical Type Theory

Consider a simple HIT, say, an HitInt:

data HitInt : Set where
  pos : (n : ℕ) → HitInt
  neg : (n : ℕ) → HitInt
  posneg : pos 0 ≡ neg 0

Or, if you don't speak Agda we can use cubicaltt:

data int = pos (n : nat)
         | neg (n : nat)
         | zeroP <i> [ (i = 0) -> pos zero
                     , (i = 1) -> neg zero ]

We want to define, for instance, a succ operation for it. As a functional programmer, we want to pattern matching on this HIT. In Agda, it's:

sucHitInt : HitInt → HitInt
sucHitInt (pos n) = pos (suc n)
sucHitInt (neg zero) = pos 1
sucHitInt (neg (suc n)) = neg n
sucHitInt (posneg x) = pos 1

Or in cubicaltt:

sucInt : int -> int = split
  pos n -> pos (suc n)
  neg n -> sucNat n
    where sucNat : nat -> int = split
            zero -> pos one
            suc n -> neg n
  zeroP @ i -> pos one

What I'm interested in is the last case-split of these two pattern matchings. The function is supposed to return the successor of the input integer, but we need to implement something that "finds the successor of the input Path".

My question is, how are we supposed to implement this case-split? In the cubicaltt version (taken from the cubicaltt's GitHub repository, examples/integer.ctt), it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer. Is this really what we want to do? Why it's not returning a Path like <i> pos 1 (even this is not a member of the higher inductive family)?

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