ยง Associativity of addition in cubicaltt

Let's first understand what we need to prove. we're trying to prove that addition is associative. addition is defined as follows: 
data nat = zero | suc (n : nat)

-- recursive on right argument
add (m : nat) : nat -> nat = split
  zero -> m
  suc n -> suc (add m n)
Since add is recursive on the right, we can simplify (by computation) values such as add x (S y) to S (add x y). This will be important when reasoning about induction later. Now, we wish to prove that: 
for all a b, c,
  a + (b + c) = (a + b) + c
we prove this by induction on c. Let's consider the base case and the inductive case: 
-- BASE CASE:
-- a + (b + 0) = (a + b) + 0
-- [computation]: a + (b) = (a + b)
By computation on the base case, we simplify (b+0) to b, and we similary simplify (a + b) + 0 to (a + b). So we're really asked to prove add a b = add a b which is trivial (by reflexivity). Next, let's think of the inductive case, where we suppose c = S n and then simplify what we have to prove to a normal form: 
-- INDUCTIVE HYPOTHESIS: let c = S n:
-- a + (b + S n) = (a + b) + S n
-- =[computation]: a + (S (b + n)) = (a + b) + S n
-- =[computation]: S (a + (b + n)) = (a + b) + S n
-- =[computation]: S (a + (b + n)) = S ((a + b) + n)
We see that after simplification by computation, we need to prove that S (a + (b + n)) = S ((a + b) + n. The core idea is to use associativity to prove that (a + (b + n)) = ((a + b) + n) and to then stick a S _ on it, giving S (a + (b + n)) = S ((a + b) + n). In a cubical diagram, this looks like: 
-- j=1
--  ^  S(a+(b+n)) - -- -- -- -- -- - S((a+b) + n)
--  |  ^                                 ^
--  |  |                             suc (add (add a b) n)
--  |  |                                 |
--  | suc(add a (add b n))            |
--  |  |                                 |
--  |  |                                 |
--  |  S(a+(b+n)) ---------------------> S((a+b)+n)
--  |           suc (add A a b n @ i)
-- j=0
-- i=0 -------------------------------> i=1
  • The bottom horizontal line is the first to comp, given as (suc (addA a b n @ i))
And in cubical code, it's written as:
  • The left and right vertical lines are the second inputs to comp.
  • The left vertical line is given by suc (add a (add b n)
  • The right vertical line is given by suc (add (add a b) n).
In total, the implementation is: 
addA (a b: nat) :
  (c: nat) -> Path nat (add a (add b c))
                       (add (add a b) c) = split
  zero ->  add a  b
  suc n ->  comp ( nat) (suc (addA a b n @ i))
                [ (i = 0) ->  suc (add a (add b n))
		        , (i = 1) ->  suc (add (add a b) n)]
EDIT: I now realise that we do not need to use comp since both the left and right edges of the square are constant. We can implement the above as: 
addA (a b: nat):
  (c: nat) -> Path nat (add a (add b c))
                       (add (add a b) c) = split
  zero ->  add a  b
  suc n ->  (suc (addA a b n @ i))