Data.Proof.EQ

Type equality proofs

Documentation

data :=: where

Type equality proof

Constructors

Refl :: a :=: a

liftEq :: (a :=: a') -> f a :=: f a'

Lift proof through a unary type constructor

liftEq2 :: (a :=: a') -> (b :=: b') -> f a b :=: f a' b'

Lift proof through a binary type constructor (including '(,)')

liftEq3 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> f a b c :=: f a' b' c'

Lift proof through a ternary type constructor (including '(,,)')

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

Lift proof through a quaternary type constructor (including '(,,,)')

commEq :: (a :=: a') -> a' :=: a

Commutativity

transEq :: (a :=: a') -> (a' :=: a'') -> a :=: a''

Transitivity