Thanks for the comments. I will take a look at the type family extension. The definition of plusFn proposed by Jim Apple worked nicely. The solution from apfelmus works after fixing a small typo:

newtype Equal a b = Proof (forall f . f a -> f b )

newtype Succ f a = InSucc { outSucc :: f (S a) }

equalZ :: Equal Z Z equalZ = Proof id

equalS :: Equal m n -> Equal (S m) (S n) -- was (S n) (S m) equalS (Proof eq) = Proof (outSucc . eq . InSucc)

plusFn :: Plus m n i -> Plus m n k -> Equal i k plusFn PlusZ PlusZ = Proof id plusFn (PlusS x) (PlusS y) = equalS (plusFn x y)

Also thanks to Derek Elkins and Dan Licata for interesting discussions about dependent sum/product. :) sincerely, Shin