[Haskell-cafe] Type equality proof

[Conor McBride]

Hi

On 17 Mar 2009, at 21:06, David Menendez wrote:

> 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

That and the identity-on-objects functor to sets and
functions.

Mutter mutter Leibniz

Conor