proposition: Corollary to_adj_counit {x} : ⌊ε⌋ ≈ id[U x].
proof: Proof. sapply (@iso_to_from Sets _ _ (@adj _ (U x) x)). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets