proposition: Theorem hom_counit_naturality_consequence {x y} (f : x ~> U y) : from hom_adj (x, y) f ≈ hom_counit _ ∘ fmap[F] f.
proof: Proof. unfold hom_counit; simpl. spose (naturality[from hom_adj] (U y, y) (x, y) (f, id) id) as X. rewrite id_left in X. rewrites. apply proper_morphism; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Theory.Adjunction Category.Adjunction.Natural.Transformation Category.Construction.Product Category.Construction.Opposite Category.Functor.Hom Category.Functor.Construction.Product Category.Functor.Opposite Category.Instance.Fun Category.Instance.Sets