[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Negation as a type family $x:A \vdash p(x):\mathbb{0}$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash \pi:\mathrm{isInequalitySpace}(A)}{\Gamma, a:A, b:A \vdash a \# b \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, \vdash \pi:\mathrm{isInequalitySpace}(A)}{\Gamma, a:A, b:A, x(a, b):a \# b, p(a, b, x):\mathbb{0} \vdash \mathrm{tight}(a, b, x, p):a =_A b}$$ lol, we just work with ordered local rings instead of ordered fields. category: redirected to nlab