proposition: Corollary from_adj_comp_law {x y} (f : x ~> U y) : ⌊⌈f⌉⌋ ≈ f.
proof: Proof. sapply (@iso_to_from Sets _ _ (@adj _ x y) f). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets