proposition: Corollary adj_univ `(f : F x ~> y) (g : x ~> U y) : f ≈ ⌈g⌉ ↔ ⌊f⌋ ≈ g.
proof: Proof. split; intros. - rewrite X. sapply (@iso_to_from Sets _ _ (@adj _ x y)). - rewrite <- X. symmetry. sapply (@iso_from_to Sets _ _ (@adj _ x y)). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets