nLab context



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels




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.


Theory of a group

In the theory of a group, it is understood that there is a group GG, that GG has various elements, that two elements of GG may be equal, that any two elements of GG have as product an element of GG, 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 GG commute will depend on (the rest of) the context.

To be more explicit, the assertion that aa and bb commute does not make sense without the additional context that aa and bb are elements of GG. Even in that context, this assertion, while at least meaningful, is not valid. However, if we add to the context the assumption that (ab) 2=a 2b 2(a b)^2 = a^2 b^2, then the assertion is valid. Written symbolically,

ab=ba \vdash\; a b = b a

is meaningless;

a:G,b:Gab=ba a\colon G,\; b\colon G \;\vdash\; a b = b a

is meaningful but invalid; and

(1)a:G,b:G,(ab) 2=a 2b 2ab=ba a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2 \;\vdash\; a b = b a

is valid.

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:

(a:G),(b:G),ab=ba \vdash\; \forall (a\colon G),\; \forall (b\colon G),\; a b = b a


(a:G),(b:G),(ab) 2=a 2b 2ab=ba \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 \forall and \Rightarrow, 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.

Split contexts

Sometimes contexts are split, where one has two different collection of contexts Γ\Gamma and Δ\Delta whose individual judgments are required to be listed separate from each other as Γ|Δ\Gamma \vert \Delta. This commonly occurs in modal type theory such as spatial type theory and cohesive homotopy type theory (specifically in real-cohesive homotopy type theory and linear homotopy type theory).


Category of contexts

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.

Categorical semantics

The categorical semantics of a context Γ\Gamma in type theory is as the slice category 𝒞 /[Γ]\mathcal{C}_{/[\Gamma]} over the object that interprets Γ\Gamma. See at categorical semantics – Definition – Of dependent type theory – Contexts and type judgements.


A comprehensive definition of categorical semantics of contexts in homotopy type theory in type-theoretic model categories is in section 2 of

Last revised on December 16, 2022 at 16:59:31. See the history of this page for a list of all contributions to it.