This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
In section 8 of the textbook, I defined rings as an abstract abelian group $(R, 0:R, +:R \times R \to R, -:R \to R)$ which additionally has the structure of elements $1:R$ and functions $(-)\cdot(-):R \times R \to R$ such that $(-)\cdot(-)$ distributes over $+$ and $1$ and $(-)\cdot(-)$ forms an associative H-space. However, on any pointed type $(A, a:A)$, any binary function $f:A \times A \to A$ induces a binary function on the loop space of $a$ by the binary action on paths of $f$, $\mathrm{ap}(f, a, a):\Omega(A, a) \times \Omega(A, a) \to \Omega(A, a)$.
This means that I could make the distinction between rings and abstract rings as the textbook does for groups and abstract groups in chapter 4, and I could define an abstract ring as above, and a ring as an abelian group $(R, \mathrm{sh}_R:B R, z_R:Z(R) \simeq R)$ with a loop $l:\Omega(B R, r)$ and a function $\mu:B R \times B R \to B R$ such that $\mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)$ distributes over concatenation of paths in the loop space $\Omega(B R, \mathrm{sh}_R)$, and $(\Omega(B R, \mathrm{sh}_R), l, \mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R))$ forms an associative H-space.
In fact, I could get rid of the requirement that group be abelian, because given a group $R$, if there is an H-space structure $(\Omega(B R, \mathrm{sh}_R), l, \mathrm{ap}(\mu))$ on the loop space of the designated shape $\mathrm{sh}_R:B R$ such that $\mathrm{ap}(\mu)$ distributes over concatenation of paths in the loop space $\Omega(B R, \mathrm{sh}_R)$, then the group is abelian, because for all paths $p:\Omega(B R, \mathrm{sh}_R)$ and $q:\Omega(B R, \mathrm{sh}_R)$, there are paths
$$p p q q = \mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)(p, l l) \mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)(q, l l) = \mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)(p q, l l)$$
$$\mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)(p q, l l)= \mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)(p q, l) \mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)(p q, l) = p q p q$$
and by the action on paths of the function $\lambda r:\Omega(B R, \mathrm{sh}_R).p^{-1} r q^{-1}$, one gets the path $p q = q p$, which implies that the group is abelian.
The results for abstract rings should follow from taking the underlying set $U(R)$ of a ring.
In section 8 of the textbook, I defined rings as an abstract abelian group $(R, 0:R, +:R \times R \to R, -:R \to R)$ which additionally has the structure of elements $1:R$ and functions $(-)\cdot(-):R \times R \to R$ such that $(-)\cdot(-)$ distributes over $+$ and $1$ and $(-)\cdot(-)$ forms an associative H-space. However, on any pointed type $(A, a:A)$, any binary function $f:A \times A \to A$ induces a binary function on the loop space of $a$ by the binary action on paths of $f$, $\mathrm{ap}(f, a, a):\Omega(A, a) \times \Omega(A, a) \to \Omega(A, a)$.
This means that I could make the distinction between rings and abstract rings as the textbook does for groups and abstract groups in chapter 4, and I could define an abstract ring as above, and a ring as an abelian group $(R, \mathrm{sh}_R:B R, z_R:Z(R) \simeq R)$ with a loop $l:\Omega(B R, r)$ and a function $\mu:B R \times B R \to B R$ such that $\mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)$ distributes over concatenation of paths in the loop space $\Omega(B R, \mathrm{sh}_R)$, and $(\Omega(B R, \mathrm{sh}_R), l, \mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R))$ forms an associative H-space.
In fact, I could get rid of the requirement that group be abelian, because given a group $R$, if there is an H-space structure $(\Omega(B R, \mathrm{sh}_R), l, \mathrm{ap}(\mu))$ on the loop space of the designated shape $\mathrm{sh}_R:B R$ such that $\mathrm{ap}(\mu)$ distributes over concatenation of paths in the loop space $\Omega(B R, \mathrm{sh}_R)$, then the group is abelian, because for all paths $p:\Omega(B R, \mathrm{sh}_R)$ and $q:\Omega(B R, \mathrm{sh}_R)$, there are paths $$p p q q = \mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)(p, l l) \mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)(q, l l) = \mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)(p q, l l)$$ $$\mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)(p q, l l)= \mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)(p q, l) \mathrm{ap}(\mu, \mathrm{sh}_R, \mathrm{sh}_R)(p q, l) = p q p q$$ and by the action on paths of the function $\lambda r:\Omega(B R, \mathrm{sh}_R).p^{-1} r q^{-1}$, one gets the path $p q = q p$, which implies that the group is abelian.
The results for abstract rings should follow from taking the underlying set $U(R)$ of a ring.