Polarity (type theory)

In type theory, a type may be classified by its polarity: either positive or negative.N.b. that "or" isn't an exclusive-or! A type may be both positive and negative. Some examples of types that are both positive and negative include the unit type 𝟏, the dependent sum Σ A P, and the Cartesian product A × B.

A positive type is uniquely characterised by the behaviour of its introduction principles; that is, the universal property characterising the type "maps outward." Positive types are defined inductively.

A negative type, however, is uniquely characterised by the behaviour of its elimination rules; the universal property characterising the type "maps inward." Negative types are defined coinductively.

References