Data.Relation.Closure.Symmetric

Definitions

data Symmetrise : Rel a -> Rel a

Totality: total
Visibility: public export
Constructors:

Fwd : r x y -> Symmetrise r x y

Bwd : r x y -> Symmetrise r y x

sym : Symmetrise r ~> flip (Symmetrise r)

Totality: total
Visibility: export

gmap : (f : (a -> b)) -> p ~> (q `on` f) -> Symmetrise p ~> (Symmetrise q `on` f)

Totality: total
Visibility: export

map : p ~> q -> Symmetrise p ~> Symmetrise q

Totality: total
Visibility: export

join : Symmetrise (Symmetrise p) ~> Symmetrise p

Totality: total
Visibility: export