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