proposition: Lemma homo_to_point_to_homo σ `{H:!rightModuleHomomorphism free_right_module rmF σ} A : point_to_homomorphism (homomorphism_to_point σ) A ∼ σ A.
proof: Proof. cbv. rewrite !cat_law3 cat_law1 !cat_law2. move: (@rm_homo _ _ _ _ _ _ _ _ _ σ H _ _ (Id (M A)))=> /= <-. rewrite -!cat_law3 -functor_law2 (relmon_law2 M). rewrite functor_law1 cat_law2 ; reflexivity. Qed.
imports: Coq(ssreflect ssrfun) Coq.Classes(RelationClasses Morphisms) Relational(Category)