## Definition ## Double negation says that given a proposition $P$ there is a function in the function type $((P \to \emptyset) \to \emptyset) \to P$. $$\frac{P\ \mathrm{type} \quad p:\prod_{a:P} \prod_{b:P} a =_P b}{q:((P \to \emptyset) \to \emptyset) \to P}$$ ### In universes ### Double negation is said to hold in a [[universe]] $\mathcal{U}$ if the universe comes with a dependent function $$p:\prod_{P:\mathcal{U}} \left(\prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:\mathcal{T}_\mathcal{U}(P)} a =_{\mathcal{T}_\mathcal{U}(P)} b\right) \to \left(((\mathcal{T}_\mathcal{U}(P) \to \emptyset) \to \emptyset) \to \mathcal{T}_\mathcal{U}(P)\right)$$ ## See also ## * [[sharp]], [[flat]], [[shape]] * [[unity of opposites]]