proposition: Corollary fmap_to_adj_counit {x y} (f : x ~{C}~> y) : fmap[U] f ≈ ⌊f ∘ ε⌋.
proof: Proof. unfold counit. rewrite to_adj_nat_r. rewrite from_adj_comp_law; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets