[Haskell-cafe] Type equality proof
conor at strictlypositive.org
Tue Mar 17 17:31:28 EDT 2009
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.
>>> 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
Mutter mutter Leibniz
More information about the Haskell-Cafe