proposition: Corollary fmap_from_adj_unit {x y} (f : x ~{D}~> y) : fmap[F] f ≈ ⌈η ∘ f⌉.
proof: Proof. unfold unit. rewrite from_adj_nat_l. rewrite to_adj_comp_law; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets