fact: Definition from {a b c} : (a → option (b → option c)) → (a + (b + (a * b)) → option c) := fun f x => match x with | inl _ => None | inr (inl _) => None | inr (inr (a, b)) => match f a with | None => None | Some k => k b end end.
imports: Category.Lib Category.Theory.Category Category.Instance.Sets Category.Structure.Cartesian