[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents \section{Apartness} Formation rule: $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash a \# b \; \mathrm{type}}$$ Introduction rule: $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash \mathrm{proptrunc}(a, b):\mathrm{isProp}(a \# b)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A \vdash \mathrm{irr}(a):(a \# a) \to \mathbb{0}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash \mathrm{sym}(a, b):(a \# b) \to (b \# a)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A, c:A \vdash \mathrm{comp}(a, b, c):(a \# c) \to ((a \# b) \vee (b \# c))}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash \mathrm{idtonotapart}(a, b):(a =_A b) \to ((a \# b) \to \mathbb{0})}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A \vdash \mathrm{idtonotapart}(a, a)(\mathrm{refl}_A(a)) \equiv \mathrm{irr}(a):(a \# a) \to \mathbb{0}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash \mathrm{tight}(a, b):\mathrm{isEquiv}(\mathrm{idtonotapart}(a, b))}$$ \section{Apartness types} An apartness type is a type $T$ with a type family $a:T, b:T \vdash a \# b \; \mathrm{type}$ and * a dependent term $a:T, b:T \vdash \mathrm{proptrunc}(a, b):\mathrm{isProp}(a \# b)$ * a dependent term $a:T \vdash \mathrm{irr}(a):(a \# a) \to \mathbb{0}$ * a dependent term $a:T, b:T \vdash \mathrm{sym}(a, b):(a \# b) \to (b \# a)$ * a dependent term $a:T, b:T, c:T \vdash \mathrm{com}(a, b, c):(a \# c) \to ((a \# b) \vee (b \# c))$ * a dependent term $a:T, b:T \vdash \mathrm{tight}(a, b):\mathrm{isEquiv}(\mathrm{idtonotapart}(a, b))$ where $a:T, b:T \vdash \mathrm{idtonotapart}(a, b):(a =_T b) \to ((a \# b) \to \mathbb{0})$ is inductively defined by $$a:T \vdash \beta_{\mathrm{idtonotapart}}^{\mathrm{refl}_T}(a):\mathrm{idtonotapart}(a, a)(\mathrm{refl}_T(a)) =_{(a \# a) \to \mathbb{0}} \mathrm{irr}(a)$$ A function $f:A \to B$ is strongly extensional if there is a dependent function $$\mathrm{strext}(a, b):(f(a) \#_B f(b)) \to (a \#_A b)$$ and the function is a strong embedding if that function is an equivalence of types $$\mathrm{stremb}(a, b):\mathrm{isEquiv}(\mathrm{strext}(a, b))$$ \section{Commutative rings} A commutative ring is a set $R$ with * a dependent term $x:R, y:R \vdash x + y:R$ * a term $0:R$ * a dependent term $x:R \vdash -x:R$ * a dependent term $x:R, y:R \vdash x \cdot y:R$ * a term $1:R$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{assoc}_+(x, y, z):x + (y + z) =_R (x + y) + z$ * a dependent term $x:R \vdash \mathrm{lunit}_+(x):0 + x =_R x$ * a dependent term $x:R \vdash \mathrm{runit}_+(x):x + 0 =_R x$ * a dependent term $x:R \vdash \mathrm{linv}_+(x):(-x) + x =_R 0$ * a dependent term $x:R \vdash \mathrm{rinv}_+(x):x + (-x) =_R 0$ * a dependent term $x:R, y:R \vdash \mathrm{comm}_+(x, y):x + y =_R y + x$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{assoc}_\cdot(x, y, z):x \cdot (y \cdot z) =_R (x \cdot y) \cdot z$ * a dependent term $x:R \vdash \mathrm{lunit}_\cdot(x):1 \cdot x =_R x$ * a dependent term $x:R \vdash \mathrm{runit}_\cdot(x):x \cdot 1 =_R x$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{ldist}_\cdot(x, y, z):x \cdot (y + z) =_R x \cdot y + x \cdot z$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{rdist}_\cdot(x, y, z):(y + z) \cdot x =_R y \cdot x + z \cdot x$ * a dependent term $x:R, y:R \vdash \mathrm{comm}_\cdot(x, y):x \cdot y =_R y \cdot x$ \section{Prefield rings} Given a commutative ring $R$, an element $a:R$ is regular if for all $b:R$, and $c:R$ the canonical functions $$\mathrm{idtoleftmul}(a, b, c):(b =_R c) \to (a \cdot b =_R a \cdot c)$$ $$\mathrm{idtorightmul}(a, b, c):(b =_R c) \to (b \cdot a =_R c \cdot a)$$ are equivalences: $$\mathrm{isRegular}(a) \coloneqq \prod_{b:A} \prod_{c:A} \mathrm{isEquiv}(\mathrm{idtoleftmul}(a, b, c)) \times \mathrm{isEquiv}(\mathrm{idtorightmul}(a, b, c))$$ We define the type of regular elements as $$\mathrm{Reg}(R) \coloneqq \sum_{a:A} \mathrm{isRegular}(a)$$ Given a commutative ring $R$, an element $a:R$ is invertible if the type of all $b:B$ such that $a \cdot b =_R 1$ is contractible $$\mathrm{isInvertible}(a) \coloneqq \mathrm{isContr}\left(\sum_{b:B} a \cdot b =_R 1\right)$$ A prefield ring is a commutative ring $R$ such that every regular element is invertible: $$\prod_{a:A} \mathrm{isRegular}(a) \simeq \mathrm{isInvertible}(a)$$ \section{Localizations and rings of fractions} Let $R$ be a commutative ring. The localization of $R$ away from an element $a:R$ is the initial commutative ring $R[a^{-1}]$ with a commutative ring homomorphism $h:R \to R[a^{-1}]$, an element $a^{-1}:R[a^{-1}]$, and an identity $\lambda_a:h(a) \cdot a^{-1} =_R 1$. Let $R$ be a commutative ring. The localization of $R$ away from a multiplicative submonoid $S$ with commutative monoid homomorphism $m:S \to R$ is the initial commutative ring $R[S^{-1}]$ with a commutative ring homomorphism $h:R \to R[S^{-1}]$, a function $(-)^{-1}:S \to R[S^{-1}]$, and identities $a:S \vdash \lambda_S(a):h(m(a)) \cdot a^{-1} =_R 1$. Let $R$ be a commutative ring. The ring of fractions $R[\mathrm{Reg}(R)^{-1}]$ is the localization of $R$ away from the monoid of regular elements $\mathrm{Reg}(R)$. The rational numbers is the ring of fractions for the integers $$\mathbb{Q} \coloneqq \mathbb{Z}[\mathrm{Reg}(\mathbb{Z})^{-1}]$$ \section{References} * Frank Quinn, *Proof Projects for Teachers* ([pdf](https://personal.math.vt.edu/fquinn/education/pfs4teachers0.pdf)) category: redirected to nlab