(R S T : Ring) : (R $-> S) -> (R $-> T) -> (R $-> S × T). Proof. intros f g. srapply Build_RingHomomorphism'. 1: apply (ab_biprod_corec f g). repeat split. 1: cbn; intros x y; apply path_prod; apply rng_homo_mult. cbn; apply path_prod; apply rng_homo_one. 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.