either

Either package contains inductive data type definition representing Sum data type. It has or synonim.

data either (A B: U) = left (a: A) | right (b: B) data or (A B: U) = inl (a: A) | inr (b: B)