eq-3.1: Leibnizian equality

Portability rank2 types, type operators, (optional) type families provisional Edward Kmett None

Data.Eq.Type

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 Source

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

Constructors

 Refl Fieldssubst :: forall c. c a -> c b

Instances

 Category := Equality forms a category Groupoid := Semigroupoid :=

# Equality as an equivalence relation

refl :: a := aSource

Equality is reflexive

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

Equality is transitive

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

Equality is symmetric

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

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

# Lifting equality

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

You can lift equality into any type constructor

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

... in any position

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

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

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