What is the type of the "adjoin" operator on rings? **Context:** I am trying to formalize the definition of a polynomial ring in a programming language. One way to think about it, is to start by formulating the definition of a ring extension by adjoining elements. In my programming formulation, I created a type for rings, and a type for variables. I am working from the following definition for polynomial rings: Let $R$ be a ring and $x$ be a variable. $R[x]$ is a polynomial ring. That is, the smallest ring that contains both $R$ and $x$. **My question:** What is the type for the 'adjoin' operator? My guess is $$[\ ]: \mbox{Ring} \times \mbox{Variable} \rightarrow \mbox{Ring}$$ (I'm just concerned with the type, not the semantics). Also, what is this called (a function that takes a ring and produces a ring)? Because I can use any properties of such operator (e.g. identity laws, associativity, etc.) in my program and do some reasoning. _Note: These are possibly the wrong tags._

That looks fine to me. In the language of category theory, "adjoin" is more than a function that produces rings from rings: it is a functor from the category of rings to itself because it also sends ring homomorphisms $R \to S$ to ring homomorphisms $R[x] \to S[x]$ in a way which satisfies certain natural compatibility conditions.