proposition: Corollary counit_comp {x y} (f : F x ~> y) : ε ∘ fmap[F] (fmap[U] f) ≈ f ∘ ε.
proof: Proof. unfold counit. rewrite <- from_adj_nat_l. rewrite <- from_adj_nat_r. rewrite id_left, id_right. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets