proposition: Theorem Adjunction_Nat_Monad : F ∹ U → @Monad D (U ◯ F).
proof: Proof. intros. unshelve econstructor; simpl; intros. - exact (transform[unit] _). - exact (fmap (transform[counit] _)). - symmetry. apply (naturality[unit]). - rewrite <- !fmap_comp. apply fmap_respects. symmetry. apply (naturality[counit]). - rewrite <- !fmap_comp. srewrite (@counit_fmap_unit); cat. - simpl. srewrite (@fmap_counit_unit); cat. - rewrite <- !fmap_comp. apply fmap_respects. symmetry. apply (naturality[counit]). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Theory.Monad Category.Theory.Adjunction Category.Adjunction.Natural.Transformation Category.Instance.Sets