proposition: Corollary from_adj_respects {x y} (f g : x ~{D}~> U y) : f ≈ g → ⌈f⌉ ≈ ⌈g⌉.
proof: Proof. intros; now rewrites. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets