How to model different logic connectivs in type theory?

Curry–Howard correspondence states type is isomorphic to logic. Be specific, type is equivalent to constructive logic. That is inhabitant of a type is a proof. Thus a type can be considered as a proposition. In other words, everything that can be written in proposition logic or first order logic should be written in type language.

Then my question is how to write various logic connectives in type language? For "conjunction (∧)" and "disjoint (∨)" I would use product type and sum type to represent them respectively, correct? But how about "negation (¬)"? I can not figure out what's the negation of a type?

Solution

Indeed, the Wikipedia article as well as most technical presentations I could find do not even mention negation: and I cannot explain why. Anyway, these are a couple of introductory articles I have been able to find that explain how the correspondence works at a more elementary/practical level:

In particular, here is how negation is explained in the first article:

Negation. This connective is the trickiest. Let's consider negation to actually be syntactic sugar. In particular, let's say that the propositional formula ~ p actually means this formula instead: p -> false. Why? The formula ~ p should mean that p does not hold. So if p did hold, then it would lead to a contradiction. Thus, given p, we could conclude false. This is the standard way of understanding negation in constructive logic.

Given that syntactic sugar, ~ p therefore corresponds to a function type whose return type is empty. Such a function could never actually return. Given our ongoing assumption that programs are total, that must mean it's impossible to even call that function. So, it must be impossible to construct a value of the function's input type. Negation therefore corresponds to the idea of impossibility, or contradiction.