proposition: Theorem Adjunction_Monad : F ⊣ U → @Monad D (U ◯ F).
proof: Proof. intros. unshelve econstructor; simpl; intros. - apply (to (adj[X])); simpl. exact id. - apply fmap. apply (from (adj[X])); simpl. exact id. - rewrite <- to_adj_nat_r. rewrite <- to_adj_nat_l. cat. - simpl. rewrite <- !fmap_comp. apply fmap_respects. rewrite <- from_adj_nat_r. rewrite <- from_adj_nat_l. cat. - rewrite <- !fmap_comp; simpl. rewrite <- from_adj_nat_l. rewrite id_left. destruct X, adj; simpl in *. rewrite iso_from_to. exact fmap_id. - rewrite <- to_adj_nat_r; simpl. rewrite id_right. destruct X, adj; simpl in *. rewrite iso_to_from. reflexivity. - rewrite <- !fmap_comp; simpl. apply fmap_respects. rewrite <- from_adj_nat_r. rewrite <- from_adj_nat_l. cat. 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