Portability | rank2 types, type operators, type families (optional) |
---|---|

Stability | provisional |

Maintainer | Edward Kmett <ekmett@gmail.com> |

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

- data a := b = Refl {
- subst :: 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

# Leibnizian equality

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