Hi
On 17 Mar 2009, at 21:06, David Menendez wrote:
2009/3/17 Luke Palmer <lrpal...@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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
