Re: [Haskell-cafe] Type equality proof

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

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

That and the identity-on-objects functor to sets and functions. Mutter mutter Leibniz Conor