fact: Definition sum_bind {A B : Type} (f : A → E + B) (o : E + A) : E + B := match o with | Datatypes.inl x => Datatypes.inl x | Datatypes.inr y => f y end.
imports: Category.Lib Category.Theory.Category Category.Structure.Cartesian Category.Structure.Cocartesian Category.Structure.Initial Category.Structure.Terminal Category.Instance.Coq Category.Theory.Coq.Semigroup Category.Theory.Coq.Monoid