4 Apr
2013
4 Apr
'13
5:38 a.m.
On 03/04/13 18:08, Richard Eisenberg wrote:
Hi all,
sym :: (a :~: b) -> (b :~: a) trans :: (a :~: b) -> (b :~: c) -> (a :~: c) coerce :: (a :~: b) -> a -> b liftEq :: (a :~: b) -> (f a :~: f b) liftEq2 :: (a :~: a') -> (b :~: b') -> (f a b :~: f a' b') liftEq3 :: ... liftEq4 :: ...
Why do you need all these lift functions? Wouldn't a single kind polymorphic one do? lift :: (f :~: g) -> (a :~: b) -> (f a :~: g b) Then you can define liftEq ab = refl `lift` ab liftEq2 ab cd = (refl `lift` ab) `lift` cd -- etc. (the name `lift` is subject to bikeshedding of course.) Twan