fact: Definition liftA2 `{Applicative F} {x y z} (f : x → y → z) (a : F x) (b : F y) : F z := ap (ap (pure f) a) b.
imports: Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Semigroup Category.Theory.Coq.Monoid