Integer and Rational Brackets as Typed Terms

This helper adopts the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices; (i) and (ii) are statements of the metatheory about expressions. Let $k\ge0$, the distinct set variables $x_{1},\dots,x_{k}$, the parameters with their fixed values, and assignments be as in Conditions Expressed by a Predicative Formula, and Guards (i); let $\gamma$ be a guard; and let terms under $\gamma$ and their values, and terms of type $A$ under $\gamma$ for a class $A$, be as in Terms and Typed Terms under a Guard (i) and Terms and Typed Terms under a Guard (ii). The brackets $[a,b]$ and $[x,m]$ below are equivalence classes, not intervals of $\mathbb{R}$, and their entries are elements of $\mathbb{N}$, respectively of $\mathbb{Z}$ and $\mathbb{N}$, not their images in $\mathbb{R}$.

(i) Let $P=\mathbb{N}\times\mathbb{N}$, $\sim$ and the classes $[a,b]$ for $a,b\in\mathbb{N}$ be as in Construction of the Integers: Pairs of Natural Numbers up to Equal Differences, with Sum, Product, Negation and Order (i), with $\mathbb{Z}=P/{\sim}$ as in The Integers (i), and let $\pi_{\sim}$ be the canonical projection of $P$ to $P/{\sim}$. Let $s$ and $t$ be terms of type $\mathbb{N}$ under $\gamma$, and let $[s,t]$ stand for the term $\pi_{\sim}((s,t))$ of Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), written with a parameter whose value is $\pi_{\sim}$. Then the value of $[s,t]$ under each assignment satisfying $\gamma$ is the class $[a,b]$, where $a$ and $b$ are the values of $s$ and $t$, and $[s,t]$ is a term of type $\mathbb{Z}$ under $\gamma$.

(ii) Let $Q=\mathbb{Z}\times\mathbb{N}$, $\approx$ and the classes $[x,m]$ for $x\in\mathbb{Z}$ and $m\in\mathbb{N}$ be as in Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order (i), with $\mathbb{Q}=Q/{\approx}$ as in The Rational Numbers (i), and let $\pi_{\approx}$ be the canonical projection of $Q$ to $Q/{\approx}$. Let $s$ be a term of type $\mathbb{Z}$ and $t$ a term of type $\mathbb{N}$ under $\gamma$, and let $[s,t]$ stand for the term $\pi_{\approx}((s,t))$ of Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), written with a parameter whose value is $\pi_{\approx}$. Then the value of $[s,t]$ under each assignment satisfying $\gamma$ is the class $[x,m]$, where $x$ and $m$ are the values of $s$ and $t$, and $[s,t]$ is a term of type $\mathbb{Q}$ under $\gamma$.