{A B C : Ring} (f : RingHomomorphism B C) (g : RingHomomorphism A B) : RingHomomorphism A C. Proof. snrapply Build_RingHomomorphism. 1: exact (f o g). rapply compose_sr_morphism. 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.