proposition: Lemma fmap_pure {a b} (f : a ~> b) : pure ∘ f ≈ fmap f ∘ pure.
proof: Proof. symmetry. sapply pure_natural. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Naturality Category.Structure.Monoidal Category.Functor.Bifunctor Category.Functor.Strong Category.Functor.Structure.Monoidal