fact: Definition Maybe_append `{Semigroup a} (x y : Maybe a) : Maybe a := match x, y with | Nothing, x => x | x, Nothing => x | Just x, Just y => Just (x ⊗ y) end.
imports: Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Applicative Category.Theory.Coq.Monad Category.Theory.Coq.Semigroup Category.Theory.Coq.Monoid Category.Theory.Coq.Traversable