natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
In type theory, a negative type is one whose eliminators are regarded as primary. Its constructors are derived from these by the rule that “to construct an element of a negative type, it is necessary and sufficient to specify how that element behaves upon applying all of the eliminators to it”.
The opposite notion is a positive type, forming two polarities.
In categorical semantics of type theory, negative types correspond to “from the right” universal properties (i.e. for mapping in).
In denotational semantics, negative types behave well with respect to “call-by-name” and other lazy evaluation? strategies.
cartesian product types can be presented both positively and negatively. The two definitions are equivalent in ordinary type theory, but distinct in linear logic. The same is true of binary sum types if we allow sequents with multiple conclusions.