Negation is the Implication of a Judgement to the bottom — the empty Judgement from which nothing follows.
Implication forces Negation: once “if A then B” exists, the question “what if B is the trivially empty Judgement?” must have an answer. The Negation of A is the Implication A → ⊥, where ⊥ is the bottom — the Judgement from which nothing follows and which says nothing.
This is constructive negation, not classical negation. In classical logic, ¬¬A = A: denying the denial of something proves it. In the Heyting algebra produced by this derivation, that does not hold. Denying the denial of A does not give you A back — it gives you something weaker. Proof of existence requires construction, not merely the refutation of non-existence.
Negation completes the Heyting algebra: Order, Meet, Join, Implication, and Negation together constitute constructive logic. This algebra constrains the syntax through Soundness, Confluence, and Normalization.
Note that Negation here — the logical operation within the Heyting algebra — recapitulates what was already present at the beginning: the negation that nothing needed in order to be nothing. What was given (pre-derivational) is now derived (produced by the algebra of Judgements).