`{Funext} (R S T : Ring) : (R $-> S) * (R $-> T) <~> (R $-> S × T). Proof. snrapply equiv_adjointify. 1: exact (uncurry (ring_product_corec _ _ _)). { intros f. exact (ring_product_fst $o f, ring_product_snd $o f). } { hnf; intros f. by apply path_hom. } intros [f g]. apply path_prod. 1,2: by apply path_hom. 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.