proposition: Theorem hom_unit_naturality_consequence {x y} (f : F x ~> y) : to hom_adj (x, y) f ≈ fmap[U] f ∘ hom_unit _.
proof: Proof. unfold hom_unit; simpl. spose (naturality[to hom_adj] (x, F x) (x, y) (id, f) id) as X. rewrite id_right 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