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

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

```
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)]

`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))
*