I'm trying to figure out to what an order relation $<$ would look like on the geometric line $R$ as defined in Kock's synthetic differential geometry.
If I understand correctly (in constructive analysis) $\mathbb{R}$ admits a linear order $<$.
Question: What would be the preferred way (if any) to define an order on $R$?
For example, if $d \in R$ satisfies the equation $d^2 = 0$, up to one of the following can be true, lest $d = 0$ be the only solution of the equation:
- $d \not< 0$ and $0 \not< d$
- $<$ is a connected irreflexive comparison, more specifically, if $x \not< y$ and $y \not< x$, then $x = y$.
I'm inclined to think 1. is true, and that $<$ defined on $R$ would be an irreflexive comparison satisfying asymmetry (i.e. $x < y \implies y \not< x$, which implies irreflexivity). I think then the preorder $ \le $ defined as the opposite of $\not<$ would end up being a total preorder, for which $d^2 = 0$ implies $d \le 0$ and $0 \le d$ (but not $d = 0$). However I haven't yet found such a relation being defined on any writing.