-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Leibnizian equality
--   
--   Leibnizian equality
@package eq
@version 0.1.0


-- | Leibnizian equality. Injectivity in the presence of type families is
--   provided by a generalization of a trick by Oleg Kiselyv posted here:
--   
--   
--   <a>http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html</a>
module Data.Eq.Type
data (:=) a b
Refl :: (forall c. c a -> c b) -> := a b
subst :: := a b -> forall c. c a -> c b
refl :: a := a
trans :: a := b -> b := c -> a := c
symm :: (a := b) -> (b := a)
coerce :: a := b -> a -> b
lift :: a := b -> f a := f b
lift2 :: a := b -> f a c := f b c
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
lower :: f a := f b -> a := b
lower2 :: f a c := f b c -> a := b
lower3 :: f a c d := f b c d -> a := b
instance Category :=