Copyright	(C) 2011-2014 Edward Kmett
License	BSD-style (see the file LICENSE)
Maintainer	Edward Kmett <ekmett@gmail.com>
Stability	provisional
Portability	rank2 types, type operators, (optional) type families
Safe Haskell	Trustworthy
Language	Haskell98

Data.Eq.Type

Contents

Description

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

Synopsis

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

Category k ((:=) k) #	Equality forms a category
Methods id :: cat a a # (.) :: cat b c -> cat a b -> cat a c #
Groupoid k ((:=) k) #
Methods inv :: k1 a b -> k1 b a #
Semigroupoid k ((:=) k) #
Methods o :: c j k1 -> c i j -> c i k1 #

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

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 #