{R : Ring} {M N : RightModule R} (R' : RightModule R) (f : R' $-> M) (g : R' $-> N) : R' $-> rm_prod M N := lm_prod_corec (R:=rng_op R) R' f g. Global Instance hasbinaryproducts_leftmodule {R : Ring} : HasBinaryProducts (LeftModule R). Proof. intros M N. snrapply Build_BinaryProduct. - exact (lm_prod M N). - exact lm_prod_fst. - exact lm_prod_snd. - exact lm_prod_corec. - cbn; reflexivity. - cbn; reflexivity. - intros L f g p q a. exact (path_prod' (p a) (q a)). Defined.
Require Import WildCat. Require Import Spaces.Nat.Core. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Groups.Kernel Algebra.Groups.Image Algebra.Groups.QuotientGroup. Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct. Require Import Rings.Ring.