|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-level 1-type/h-prop|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator monad||modal type theory, monad (in computer science)|
In type theory, a positive type is one whose constructors are regarded as primary. Its eliminators are derived from these by the rule that “to use an element of a positive type, it is necessary and sufficient to specify what should be done for all possible ways that element could have been constructed”.
The opposite notion is a negative type.
In categorical semantics of type theory, positive types correspond to “from the left” universal properties (i.e. for mapping out).
cartesian product types can be presented both positively (as a particular inductive type) and negatively. The two definitions are equivalent in ordinary type theory, but distinct in linear logic. The same is true for binary sum types if we allow sequents with multiple conclusions.