Category instance for algebras over a commutative ring #
We introduce the bundled category
AlgebraCat of algebras over a fixed commutative ring
with the forgetful functors to
ModuleCat. We furthermore show that the functor
associating to a type the free
R-algebra on that type is left adjoint to the forgetful functor.