proposition: Corollary adj_univ_impl {x y} (f : F x ~> y) (g : x ~> U y) : f ≈ ε ∘ fmap[F] g ↔ ⌊f⌋ ≈ g.
proof: Proof. unfold counit. split; intros. - rewrite X; clear X. rewrite <- from_adj_nat_l. rewrite id_left. apply from_adj_comp_law. - rewrite <- X; clear X. rewrite <- from_adj_nat_l. rewrite id_left. symmetry. apply to_adj_comp_law. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets