[Haskell-cafe] Type equality proof

[David Menendez]

2009/3/17 Luke Palmer <lrpalmer at gmail.com>:
>> 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 <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>