TypeAligned.Sum

Sum type for binary relations.

Definitions

data Sum : Rel a -> Rel a -> Rel a

  Sum / Either of relations (linear!)

Totality: total
Visibility: public export
Constructors:

Left : p x y -@ Sum p q x y

Right : q x y -@ Sum p q x y

Hints:

(Eq (p x y), Eq (q x y)) => Eq (Sum p q x y)

(Show (p x y), Show (q x y)) => Show (Sum p q x y)

bimapOnce : {0 f : a -> b} -> p x y -@ r (f x) (f y) -> q x y -@ s (f x) (f y) -> Sum p q x y -@ Sum r s (f x) (f y)

  Linear 'bimap'

Totality: total
Visibility: export

bimap : {0 f : a -> b} -> (p x y -> r (f x) (f y)) -> (q x y -> s (f x) (f y)) -> Sum p q x y -> Sum r s (f x) (f y)

  Transform relationships

Totality: total
Visibility: export