|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 logic and type theory, the context of a judgement (or hypothetical judgement, with dependence on the context) consists of all of the assumptions that are made when that assertion is claimed to be valid; whether an assertion is in fact valid (or even meaningful) may depend on the context. The precise definition depends on the theory (or doctrine) that one is working in.
Generally, a context is thought of as relative to some underlying logical theory. This underlying theory will contain most of the assumptions of what constitutes validity; the context of an assertion in this theory will then include only those extra assumptions that may be used by that assertion. On the other hand, one could also think of the entire base theory as part of the context.
In the theory of a group, it is understood that there is a group , that has various elements, that two elements of may be equal, that any two elements of have as product an element of , and that various equational laws are satisfied (which we will not list here). That is all taken for granted when discussing a group. However, the validity and meaningfulness of an assertion that two elements of commute will depend on (the rest of) the context.
To be more explicit, the assertion that and commute does not make sense without the additional context that and are elements of . Even in that context, this assertion, while at least meaningful, is not valid. However, if we add to the context the assumption that , then the assertion is valid. Written symbolically,
\vdash\; a b = b a
a\colon G,\; b\colon G \;\vdash\; a b = b a
is meaningful but invalid; and
a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2 \;\vdash\; a b = b a
In a sufficiently rich logical language, contexts are unnecessary, which is why contexts are not usually explained in accounts of logic for ordinary reasoning (including in ordinary mathematics). For example, the two meaningful assertions above may be rewritten thus:
\vdash\; \forall (a\colon G),\; \forall (b\colon G),\; a b = b a
\vdash\; \forall (a\colon G),\; \forall (b\colon G),\; (a b)^2 = a^2 b^2 \;\Rightarrow\; a b = b a
Here the context on the left side is the empty context, consisting of no assumptions whatsoever (beyond those underlying the base theory).
However, these versions involve and , while the previous versions work in weaker logics. In fact, these assertions make sense (and the valid one may be proved) in the internal logic of a group object in a finitely complete category (and somewhat more generally than that). Accordingly, they can be interpreted as statements about any group object in any finitely complete category (and the valid one will then be interpreted as a true statement), exactly as they do for groups (which are group objects in the finitely complete category Set).
Even if one is completely uninterested in internalization or weak logics, a basic familiarity with contexts may help drive home a point that is important throughout reasoning: What you can state and prove depends on your assumptions.
The category of contexts in a theory forms its syntactic category, which is a split model of type theory and is important in the relation between type theory and category theory. See Categorical semantics below.
The categorical semantics of a context in type theory is as the slice category over the object the interprets . See at categorical semantics – Definition – Of dependent type theory – Contexts and type judgements.