fact: Definition mapLeft `(f : a → c) `(x : a + b) : c + b := match x with | inl l => inl (f l) | inr r => inr r end.
imports: Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Applicative Category.Theory.Coq.Monad