Data.Eq.Type

Equality

data a := b where

Constructors

Refl :: a := a

Instances

Category :=

Semigroupoid :=

Equality as an equivalence relation

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

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

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

Lifting equality

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

Lowering equality

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