proposition: Lemma point_to_homomorphism_to_point η A : homomorphism_to_point (point_to_homomorphism η) A ∼ η A.
proof: Proof. cbv. rewrite !cat_law1 cat_law2 -cat_law3 nt_natural cat_law3 -(rm_law3 rmF) cat_law1 rm_law1 cat_law1; reflexivity. Qed.
imports: Coq(ssreflect ssrfun) Coq.Classes(RelationClasses Morphisms) Relational(Category)