0
$\begingroup$

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)
```
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.