David Corfield polarity

polarity in type theory

Positive types are inductively defined by their introduction rules and correspond to colimits and other “mapping-out” universal properties; negative types are coinductively defined by their elimination rules and correspond to limits and other “mapping-in” universal properties.

positive propositions are “defined” by their form of introduction, and negative propositions by their form of elimination. In Dummett’s sense, positive propositions have a “verificationist meaning-theory”, and negative propositions a “pragmatist meaning-theory”. (Zeilberger)

Harper’s post

Of definitions of product:

Negative: Method 1 is a formulation of the idea that a proof of a conjunction is anything that behaves conjunctively, which means that it supports the two elimination rules given in the definition. There is no commitment to the internal structure of a proof, nor to the details of how projection operates; as long as there are projections, then we are satisfied that the connective is indeed conjunction. We may consider that the elimination rules define the connective, and that the introduction rule is derived from that requirement. Equivalently we may think of the proofs of conjunction as being coinductively defined to be as large as possible, as long as the projections are available.

Positive: Method is a direct formulation of the idea that the proofs of a conjunction are inductively defined to be as small as possible, as long as the introduction rule is valid. Specifically, the single introduction rule may be understood as defining the structure of the sole form of proof of a conjunction, and the single elimination rule expresses the induction, or recursion, principle associated with that viewpoint. Specifically, to reason from the fact that $A\wedge B\;\text{true}$ to derive $C\;\text{true}$, it is enough to reason from the data that went into the proof of the conjunction to derive $C\;\text{true}$. We may consider that the introduction rule defines the connective, and that the elimination rule is derived from that definition.

• type former models a right adjoint, its elimination rule(s) are modeled by the counit of the adjunction and its introduction rule is given by one direction of the Hom isomorphism.

• type former models a left adjoint, its introduction rule(s) are modeled by the unit of the adjunction and its introduction rule is given by the opposite direction of the Hom isomorphism.

So product:

• As right adjoint to duplication, elimination rules pair to give counit.

• Representation in a multicategory: $A, B \vdash A \times B$ is unit, intro rules. Elimination is one way in Hom isomorphism $Hom((A, B), C) \cong Hom(A \times B, C)$.