proposition: Corollary from_adj_unit {x} : ⌈η⌉ ≈ id[F x].
proof: Proof. 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