[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Mathematics without forall and implication: We take coherent mathematics and add logical equivalence and negation. Also, useful for mathematics done in a category whose subobject posets are $\sigma$-frames. \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{Categorical semantics} * [[Michael Shulman]] (2018). Comparing material and structural set theories. [arXiv:1808.05204](https://arxiv.org/abs/1808.05204). We should figure out where forming the set of bijections lies on the tower of impredicativity. function sets -> fullness -> power sets \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$ \section{Cauchy sequences} sequential Cauchy completion as syntactic rules. $$\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}$$ category: redirected to nlab