proposition: Corollary counit_fmap_unit {x} : ε ∘ fmap[F] η ≈ id[F x].
proof: Proof. unfold unit, counit. rewrite <- from_adj_nat_l; cat. sapply (@iso_from_to Sets _ _ (@adj _ x (F x))). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets