## § 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)
--  |  ^                                 ^
--  |  |                                 |
--  |  |                                 |
--  |  |                                 |
--  |  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) :

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):