Data.Eq.Type

Leibnizian equality. Injectivity in the presence of type families is provided by a generalization of a trick by Oleg Kiselyv posted here:

http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html

Leibnizian equality

data a := b infixl 4

Leibnizian equality states that two things are equal if you can substite one for the other in all contexts

Constructors

Refl

Fields

subst :: forall c. c a -> c b

Instances

Groupoid (:=)

Semigroupoid (:=)

Category * (:=)

Equality forms a category

Equality as an equivalence relation

refl :: a := a

Equality is reflexive

trans :: (a := b) -> (b := c) -> a := c

Equality is transitive

symm :: (a := b) -> b := a

Equality is symmetric

coerce :: (a := b) -> a -> b

If two things are equal you can convert one to the other

Lifting equality

lift :: (a := b) -> f a := f b

You can lift equality into any type constructor

lift2 :: (a := b) -> f a c := f b c

... in any position

lift2' :: (a := b) -> (c := d) -> f a c := f b d

lift3 :: (a := b) -> f a c d := f b c d

lift3' :: (a := b) -> (c := d) -> (e := f) -> g a c e := g b d f

Lowering equality

lower :: (f a := f b) -> a := b

Type constructors are injective, so you can lower equality through any type constructor

lower2 :: (f a c := f b c) -> a := b

... in any position

lower3 :: (f a c d := f b c d) -> a := b