I am attempting to develop a theory of rings which features quotients. So far, I have defined rings through axiomatic classes and ideals through a predicate constant. There are several approaches to defining the quotient ring which present themselves, but the next step would be to prove that the quotient is an instance of the ring class. Is there a straightforward way to do this without specifying a particular ideal? My goal, as I imagine it, is to define a type which is parameterized, essentially, by subsets of "UNIV::('a::ring set)" (or more specifically, by subsets which satisfy my is_ideal predicate). Is this possible? Is there a different (better) way to approach this problem?