[Agda] simple question

[Mateusz Kowalczyk]

On 10/14/2014 03:13 AM, Andrew Harris wrote:
> Hello,
> 
>    I'm trying to follow along in the very good paper "Dependent Types At
> Work" written by Ana Bove and Peter Dybjer.  I'm stuck at trying to prove
> "eq-succ", which is one of the exercises in Section 4.4.  The closest I can
> make it is the following:
> 
> {- proof of eq-succ -}
> eq-succ : {n m : Nat} → n == m → succ n == succ m
> eq-succ (refl m) = natrec {(\k → (k + m) == (plus k m))} (refl m) (\i h →
> ((succ i) + m) == (plus (succ i) m)) m
> 
> But this does not typecheck, I get the error:
> 
> Set !=< (succ i + m) == plus (succ i) m of type Set₁
> when checking that the expression (succ i + m) == plus (succ i) m
> has type (succ i + m) == plus (succ i) m
> 
> I'm stuck -- I don't quite understand what I'm supposed to create an
> element of Set_1 that has a signature of (succ i + m) == plus (succ i) m, (if
> that's what I'm supposed to do).  Any hints would be appreciated!
> 
> -andrew
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

This is probably a stupid question considering I haven't looked at the
cited work, but what's wrong with just ‘cong suc’?

-- 
Mateusz K.