Given a statement regarding the category C, by interchanging the source and target of each morphism as well as interchanging the order of composing two morphisms, a corresponding dual statement is obtained regarding the opposite category Cop.
In the case when C and its opposite Cop are equivalent, such a category is self-dual.
In applications to logic, this then looks like a very general description of negation (that is, proofs run in the opposite direction).
For example, if we take the opposite of a lattice, we will find that meets and joins have their roles interchanged.
This is an abstract form of De Morgan's laws, or of duality applied to lattices.