Ring -> Ring -> Ring. Proof. intros R S. snrapply Build_Ring. - exact (ab_biprod R S). - exact (fun '(r1 , s1) '(r2 , s2) => (r1 * r2 , s1 * s2)). - exact (ring_one , ring_one). - intros [r1 s1] [r2 s2] [r3 s3]. apply path_prod; cbn; apply rng_mult_assoc. - intros [r1 s1] [r2 s2] [r3 s3]. apply path_prod; cbn; apply rng_dist_l. - intros [r1 s1] [r2 s2] [r3 s3]. apply path_prod; cbn; apply rng_dist_r. - intros [r1 s1]; apply path_prod; cbn; apply rng_mult_one_l. - intros [r1 s1]; apply path_prod; cbn; apply rng_mult_one_r. Defined.
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.