Ceiling $⊣$ inclusion $⊣$ floor: an adjoint triple between $(\mathbb{R},\le )$ and $(\mathbb{Z},\le )$

Three nonstrict consequences of [F7], each obtained by adjoining the equality case to a strict statement, are used below. (a) $t\le u$ exactly when $t+v\le u+v$: if $t<u$ then $t+v<u+v$ by [F7] and if $t=u$ then $t+v=u+v$, so $t+v\le u+v$; applying the same with $-v$ recovers $t\le u$. (b) $t\le u$ exactly when $-u\le -t$: translating by $v=-t-u$ carries the first to the second by (a), and translating by $t+u$ carries it back. (c) If $t\le u<w$ then $t<w$: for $t<u$ this is transitivity of the strict order and for $t=u$ it is immediate.

An integer $d$ with $d<1$ satisfies $d\le 0$. The order of $\mathbb{Z}$ is total by [F5], so either $d\le 0$ or $0<d$. In the second case $d\ge 0$ and $d\mathrm{\ne }0$, so [F5] presents $d$ as the image of a unique natural $j$, with $j\mathrm{\ne }0$ because the embedding is injective and sends $0$ to $0$; then $0<j$, so [F6] with $m=0$ gives $\sigma (0)=1\le j$, and the embedding preserves order and $1$, so $1\le d$. That contradicts $d<1$ by trichotomy, leaving $d\le 0$.

$\lfloor J(m)\rfloor =m$ for every integer $m$. Indeed $m\le J(m)<m+1$ holds because $J(m)$ is $m$ read in $\mathbb{R}$ and $0<1$ there, so the uniqueness clause of [F4] identifies $\lfloor J(m)\rfloor$ with $m$.

For every integer $m$ and real $x$: $J(m)\le x$ exactly when $m\le \lfloor x\rfloor$. If $m\le \lfloor x\rfloor$ then, since $\lfloor x\rfloor \le x$ by [F4] and $J$ preserves order by [F5], transitivity gives $J(m)\le x$. Conversely suppose $J(m)\le x$. By [F4] also $x<\lfloor x\rfloor +1$, so $m<\lfloor x\rfloor +1$ by step 1.1(c), and translating by $-\lfloor x\rfloor$ with [F7] turns this into $m-\lfloor x\rfloor <1$. Now $m-\lfloor x\rfloor$ is an integer by [F5], so step 1.2 gives $m-\lfloor x\rfloor \le 0$, that is $m\le \lfloor x\rfloor$.

$\lceil J(m)\rceil =m$ for every integer $m$: $-m$ is an integer with $J(-m)=-J(m)$ by [F5], and step 1.3 gives $\lfloor J(-m)\rfloor =-m$, whence $\lceil J(m)\rceil =-\lfloor -J(m)\rfloor =-\lfloor J(-m)\rfloor =m$.

$J$ and $\lfloor -\rfloor$ are monotone, and $J⊣\lfloor -\rfloor$. That $J$ is monotone is part of [F5]. If $x\le y$ then $J(\lfloor x\rfloor )\le x\le y$ by [F4], so step 2.1 applied to the integer $\lfloor x\rfloor$ and the real $y$ gives $\lfloor x\rfloor \le \lfloor y\rfloor$; thus $\lfloor -\rfloor$ is monotone. The equivalence of step 2.1 is then exactly the condition in [F2] for $J⊣\lfloor -\rfloor$, whose unit is $m\le \lfloor J(m)\rfloor$ and whose counit is $J(\lfloor x\rfloor )\le x$.

For every integer $m$ and real $x$: $\lceil x\rceil \le m$ exactly when $x\le J(m)$. By step 1.1(b), $x\le J(m)$ exactly when $-J(m)\le -x$, and $-J(m)=J(-m)$ because $J$ preserves addition and $0$ by [F5]. Step 2.1, applied to the integer $-m$ and the real $-x$, converts $J(-m)\le -x$ into $-m\le \lfloor -x\rfloor$, and step 1.1(b) converts that into $-\lfloor -x\rfloor \le m$, which is $\lceil x\rceil \le m$.

$\lceil -\rceil$ is monotone and $\lceil -\rceil ⊣J$. If $x\le y$ then $-y\le -x$ by step 1.1(b), so $\lfloor -y\rfloor \le \lfloor -x\rfloor$ by step 3.1, and step 1.1(b) gives $-\lfloor -x\rfloor \le -\lfloor -y\rfloor$, that is $\lceil x\rceil \le \lceil y\rceil$. With $J$ monotone by [F5], the equivalence of step 3.2 is the condition in [F2] for $\lceil -\rceil ⊣J$, whose unit is $x\le J(\lceil x\rceil )$ and whose counit is $\lceil J(m)\rceil \le m$.

Taking $\mathcal{C}=(\mathbb{Z},\le )$ and $\mathcal{D}=(\mathbb{R},\le )$ as thin categories by [F1], with $M=J$ and $L=\lceil -\rceil$, $R=\lfloor -\rfloor$, steps 3.1 and 4.1 supply the two adjunctions $L⊣M$ and $M⊣R$ required by [F3]. Hence $\lceil -\rceil ⊣J⊣\lfloor -\rfloor$ is an adjoint triple.

The counit of $J⊣\lfloor -\rfloor$ and the unit of $\lceil -\rceil ⊣J$ are in general strict, while steps 1.3 and 2.2 make the other unit and counit equalities. For $x=\frac{1}{2}$: $[F4]$ applied to $0\le \frac{1}{2}<1$ gives $\lfloor x\rfloor =0$, so $J(\lfloor x\rfloor )=0<\frac{1}{2}$; and applied to $-1\le -\frac{1}{2}<0$ it gives $\lfloor -x\rfloor =-1$, so $\lceil x\rceil =1$ and $\frac{1}{2}<1=J(\lceil x\rceil )$.