[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] The Riemann series theorem in constructive mathematics... 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