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