I'm new to Cubical Agda and I am trying to define the dependent set eliminator for certain quotient types.

In particular, my quotient type is the integers, quotiented by the absolute value function (Int / rInt), defined as follows:

data Int : Set where
  pos : (n : Nat) → Int
  neg : (n : Nat) → Int

rNat : Nat -> Nat -> Type
rNat zero zero = True
rNat zero (suc b) = ⊥
rNat (suc a) zero = ⊥
rNat (suc a) (suc b) = rNat a b

abs : Int -> Nat
abs (pos x) = x
abs (neg x) = x

rNatEq : (a : Nat) -> (b : Nat) → (rNat a b) → a ≡ b
rNatEq zero zero x = refl
rNatEq (suc a) (suc b) x = cong suc (rNatEq a b x)

rInt : Int -> Int -> Type
rInt a b = rNat (abs a) (abs b)

I wish to prove/define the following hole:

depElimSetInt/rInt : (P : Int / rInt -> Set) -> (∀ x -> isSet (P x)) -> (P depConstrInt/rInt0) -> (∀ n -> (P n) -> P (depConstrInt/rIntS n)) -> ((x : Int / rInt) -> P x)
depElimSetInt/rInt P set baseCase sucCase = SetQuotients.elim set lem wellDefined where
  lem : (a : Int) → P [ a ]
  lem (pos zero) = baseCase
  lem (pos (suc n)) =  sucCase [ pos n ] (lem (pos n))
  lem (neg zero) = transport (cong P (rIntPosNegQ 0)) baseCase
  lem (neg (suc n)) = transport (cong P (rIntPosNegQ (suc n))) (sucCase [ pos n ] (lem (pos n)))
  wellDefined : (a b : Int) (r : rInt a b) → PathP (λ i → P (eq/ a b r i)) (lem a) (lem b)
  wellDefined = {!!}

where depConstrInt/rInt0 corresponds to my base case:

depConstrInt/rInt0 : Int / rInt
depConstrInt/rInt0 = [ pos 0 ]

and depConstrInt/rIntS corresponds to succesion over my quotiented integers:

depConstrInt/rIntS : Int / rInt -> Int / rInt
depConstrInt/rIntS = sucInt/rInt

wellDefined is intuitively true because the construction of r means that lem a and lem b should relate under the equivalence relation (rInt).

As lemmas, I've proven some theorems that I think may help:

rNatEquiv : (a : Nat) -> (rNat a a)
rNatEquiv zero = tt
rNatEquiv (suc a) = rNatEquiv a

rIntPosNeg : (n : Nat) → (rInt (pos n) (neg n))
rIntPosNeg n = rNatEquiv n

rIntPosNegQ : (n : Nat) -> ([_] {A = Int} {R = rInt} (pos n)  ≡ [_] {A = Int} {R = rInt} (neg n))
rIntPosNegQ n = eq/ (pos n) (neg n) (rIntPosNeg n)

rIntEquivGen : (a : Int) -> (b : Int) -> (r : rInt a b) → ([ a ] ≡ [ b ]) ≡ ([ a ] ≡ [ a ])
rIntEquivGen a b r = subst (λ x → ([ a ] ≡ x) ≡ (([_] {R = rInt} a) ≡ [ a ])) (eq/ {R = rInt} a b r) refl

I've attempted to prove this via congP, transport, and subst, with the lemmas I have already shown, but am not sure if this is the right strategy. Thanks!