Data.Setoid.Either

Coproduct of setoids

Definitions

data Or : Rel a -> Rel b -> Rel (Either a b)

  Binary relation disjunction

Totality: total
Visibility: public export
Constructors:

Left : p x y -> Or p q (Left x) (Left y)

Right : q x y -> Or p q (Right x) (Right y)

Either : Setoid -> Setoid -> Setoid

  Coproduct of setoids

Totality: total
Visibility: public export

Left : a ~> Either a b

  Setoid homomorphism smart constructor

Totality: total
Visibility: public export

Right : b ~> Either a b

  Setoid homomorphism smart constructor

Totality: total
Visibility: public export

either : a ~> c -> b ~> c -> Either a b ~> c

  Setoid homomorphism deconstructor

Totality: total
Visibility: public export