# CubicalTT: successor of add proof?

Lecture 2 of the cubical type theory lectures provide a proof of (suc a) + b = suc (a + b):

-- (suc a) + b = suc (a + b)
addSuc (a : nat) : (b : nat) -> Path nat (add (suc a) b) (suc (add a b)) = split
zero -> <i> suc a
suc n -> <i> suc (addSuc a n @ i)


I'm trying to move the (b : nat) from the return type to the argument type, such that the declaration is now addSuc2 (a b : nat) : Path nat ....

-- |Type checking failed: infer addSuc2
addSuc2 (a b : nat) : Path nat (add (suc a) b) (suc (add a b)) = split
zero -> split@(nat -> Path nat (add (suc a) b) (suc (add a b))) with
zero -> <i> suc a
suc b' -> <i> suc a
suc n -> split@(Path nat (add (suc a) b) (suc (add a b))) with
zero -> <i> suc (addSuc a n @ i)
suc b' -> <i> suc (addSuc a n @ i)


Unfortunately, this fails type checking with a cryptic infer addSuc2. I'm unable to deduce how to fix this. (a) How do I define addSuc2 such that it typechecks? (b) If it is impossible to define addSuc2, why?

Full reproducer:

module addzero where
data nat = zero | suc (n : nat)

add (m : nat) : nat -> nat = split
zero -> m
suc n -> suc (add m n)

Path (A : U) (a b : A) : U = PathP (<_> A) a b

-- (suc a) + b = suc (a + b)
addSuc (a : nat) : (b : nat) -> Path nat (add (suc a) b) (suc (add a b)) = split
zero -> <i> suc a
suc n -> <i> suc (addSuc a n @ i)

-- | This fails type checking x(
addSuc2 (a b : nat) : Path nat (add (suc a) b) (suc (add a b)) = split
zero -> split@(nat -> Path nat (add (suc a) b) (suc (add a b))) with
zero -> <i> suc a
suc b' -> <i> suc a
suc n -> split@(Path nat (add (suc a) b) (suc (add a b))) with
zero -> <i> suc (addSuc a n @ i)
suc b' -> <i> suc (addSuc a n @ i)
$$$$
`