Homotopy Type Theory algebra (ring theory) > history (Rev #4)

Definition

Given a ring $R$, an $R$-algebra is a ring $A$ with a ring homomorphism? $f:R \to A$.