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 argumentadd (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))