proposition: Corollary to_adj_unit {x y} (f : F x ~> y) : ⌊f⌋ ≈ fmap[U] f ∘ η.
proof: Proof. rewrite <- (id_right f). rewrite to_adj_nat_r. rewrite fmap_comp; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets