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


-- | Leibnizian equality
--   
--   Leibnizian equality.
@package eq
@version 4.1


-- | Leibnizian equality. Injectivity in the presence of type families is
--   provided by a generalization of a trick by Oleg Kiselyov posted here:
--   
--   
--   <a>http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html</a>
module Data.Eq.Type

-- | Leibnizian equality states that two things are equal if you can
--   substitute one for the other in all contexts
newtype a (:=) b
Refl :: (forall c. c a -> c b) -> (:=) a b
[subst] :: (:=) a b -> forall c. c a -> c b

-- | Equality is reflexive
refl :: a := a

-- | Equality is transitive
trans :: a := b -> b := c -> a := c

-- | Equality is symmetric
symm :: (a := b) -> (b := a)

-- | If two things are equal you can convert one to the other
coerce :: a := b -> a -> b

-- | You can lift equality into any type constructor
lift :: a := b -> f a := f b

-- | ... in any position
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

-- | Type constructors are injective, so you can lower equality through any
--   type constructor
lower :: forall (a :: *) (b :: *) (f :: * -> *). f a := f b -> a := b

-- | ... in any position
lower2 :: forall (a :: *) (b :: *) (c :: *) (f :: * -> * -> *). f a c := f b c -> a := b

-- | But unfortunately these definitions aren't polykinded. Everything is
--   just a star.
lower3 :: forall (a :: *) (b :: *) (c :: *) (d :: *) (f :: * -> * -> * -> *). f a c d := f b c d -> a := b
fromLeibniz :: a := b -> a :~: b
toLeibniz :: a :~: b -> a := b
reprLeibniz :: a := b -> Coercion a b
instance Control.Category.Category (Data.Eq.Type.:=)
instance Data.Semigroupoid.Semigroupoid (Data.Eq.Type.:=)
instance Data.Groupoid.Groupoid (Data.Eq.Type.:=)
instance forall k (a :: k). Data.Type.Equality.TestEquality ((Data.Eq.Type.:=) a)
instance forall k (a :: k). Data.Type.Coercion.TestCoercion ((Data.Eq.Type.:=) a)