Re: [Haskell-cafe] Type equality proof

2009/3/17 Luke Palmer :

...

Here are the original definition and the proofs of comm and trans. Compiles fine with GHC 6.10.1.

   data (a :=: a') where

       Refl :: a :=: a

   comm :: (a :=: a') -> (a' :=: a)    comm Refl = Refl

   trans :: (a :=: a') -> (a' :=: a'') -> (a :=: a'')    trans Refl Refl = Refl

These two theorems should be in the package.

How about this? instance Category (:=:) where id = Refl Refl . Refl = Refl -- Dave Menendez http://www.eyrie.org/~zednenem/