proposition: Lemma pure_natural : natural (@pure).
proof: Proof. simpl; intros. unfold pure. normal. rewrite to_unit_right_natural. rewrite fmap_comp. rewrite <- !comp_assoc. apply compose_respects; [reflexivity|]. spose (strength_natural _ _ g I I id) as X. normal. rewrites. rewrite <- !comp_assoc. apply compose_respects; [reflexivity|]. rewrite <- from_unit_right_natural. rewrite !comp_assoc. apply compose_respects; [|reflexivity]. normal. rewrite fmap_id; cat. 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