[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] The Riemann series theorem in constructive mathematics is false. What about a weaker version of the Riemann series theorem? $$\frac{\Gamma, n:\mathbb{N} \vdash a(n):R \quad \Gamma, \epsilon:R_+ \vdash M(\epsilon):\mathbb{N} \quad \Gamma, \epsilon:R_+, i:\mathbb{N}, p:i \geq M(\epsilon), j:\mathbb{N}, q:j \geq M(\epsilon) \vdash r(\epsilon, i, p, j, q):a(i) \sim_\epsilon a(j)}{\Gamma \vdash \lim_{n \to \infty} a(n):R}$$ sequential Cauchy completion as syntactic rules. Mathematics without forall and implication: We take coherent mathematics and add logical equivalence and negation. \section{Negation} Negation as being equivalent to the empty type ... Let $A$ be a type. We define $\neg A \coloneqq (A \simeq \mathbb{0})$ as the equivalence type between $A$ and the empty type $\mathbb{0}$. \section{Tight apartness} An tight apartness relation is a relation which is irreflexive, symmetric, comparative, and type, a type family * $x:A, y:A \vdash R(x, y) \; \mathrm{type}$ which comes with * $x:A, y:A, p:R(x, y), q:R(x, y) \vdash \mathrm{proptrunc}(x, y, p, q):p =_{R(x, y)} q$ * $x:A \vdash \mathrm{irr}(x):R(x, x) \simeq \mathbb{0}$ * $x:A, y:A, p:R(x, y) \vdash \mathrm{sym}(x, y, p):R(y, x)$ * $x:A, y:A, z:A, p:R(x, z) \vdash \mathrm{comp}(x, y, z, p):\left[R(x, y) + R(y, z)\right]$ * $x:A, y:A, p:R(x, x) \simeq \mathbb{0} \vdash \mathrm{tight}(x, y, p):x =_A y$ category: redirected to nlab