Homotopy Type Theory Sandbox (Rev #71, changes)

Invertible elements

Given a commutative ring $R$, a term $e:R$ is left invertible if the fiber of right multiplication by $e$ at $1$ is inhabited.

A term $e:R$ is right invertible if the fiber of left multiplication by $e$ at $1$ is inhabited.

An term $e:R$ is invertible or a unit if it is both left invertible and right invertible.

The multiplicative group of units invertible elements in$R$ is the subset subgroup of all units invertible elements in$R$

Non-cancellative Non-regular and non-invertible elements

Given An a element commutative ring$x:R$ R x:R , the is monoid non-regular of if cancellative elements in$\mathrm{<span><del\; class="diffmod">\; R</del><ins\; class="diffmod">\; x</ins></span>}$ R x is being denoted regular as implies that$\mathrm{Can}0<span><del\; class="diffmod">\; (</del><ins\; class="diffmod">\; =</ins></span>R1)$ \mathrm{Can}(R) 0 = 1 with injection $i:\mathrm{Can}(R) \to R$ and the group of units is denoted as $R^\times$ with injection $j:R^\times \to R$. An element $x \in R$ is non-cancellative if for all elements $y \in \mathrm{Can}(R)$, if $i(y) = x$, then $0 = 1$. An element $x \in R$ is non-invertible if for all elements $y \in R^\times$, if $j(y) = x$, then $0 = 1$.