nLab variable



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, a variable is a symbol that stands for an arbitrary instantiation of some given type (although in single-typed theories the type is trivial). Thus, every variable of type TT is a term of type TT (although typically there are other terms).

Logicians have developed several ways to precisely specify what variables are and how to keep track of them, and the only thing more annoyingly pedantic than learning one of these is translating between different ones.

Free and bound variables

If we keep track of context, every introduction of a variable changes the context. Thus, whatever terms of type TT there may (or may not) be in a given context Γ\Gamma, in the context (Γ,x:T)(\Gamma, x\colon T) —which is Γ\Gamma extended by a free variable xx of type TT— there is (at least) one more term of type TT, and that term is xx itself.

Conversely, we may be able to take a term aa in the context (Γ,x:T)(\Gamma, x\colon T) and apply some operation ff to it to create a term f(a)f(a) (possibly of a different type) in the context Γ\Gamma; then any appearances of the variable xx in the term aa have become bound variables in the term f(a)f(a). That is, the appearances of xx are bound by the operator ff, and xx has no meaning outside of its scope.

So for example, if (say in something simple like Peano arithmetic, supplemented with the abbreviations used in practice) I write 2x2x, this is a term (for a natural number) in a context with a free variable xx, whereas if I write 3 x=0 42x+53 \sum_{x=0}^4 2x + 5, this is a term (also for a natural number) in a context with no free variables; here, xx is bound. The variable xx has a meaning after the operator x=0 4\sum_{x=0}^4 (whose notation also specifies the variable that will have a meaning inside it) and before the plus sign (which, following the standard order of operations, marks the end of the scope of x=0 4\sum_{x=0}^4) but has no meaning outside of that (where the 33 and 55 are, or even where the 00 and 44 are). And indeed, the ultimate meaning of 2x2x depends on what xx is, but the ultimate meaning of 3 x=0 42x+53 \sum_{x=0}^4 2x + 5 is simply 6565.

In categorical semantics

In the internal language of a category 𝒞\mathcal{C} a morphism

f:BA f\colon B \to A

is a term f(x)f(x) of type AA where xx is a free variable of type BB, which in symbols is given by

x:Bf(x):A. x\colon B \vdash f(x)\colon A \,.

We may think of the free variables here as being placeholders for all the generalized elements UxBU \stackrel{x}{\to} B of BB.

Then the assertion

x:Bf(x):A x\colon B \vdash f(x)\colon A

indicates that with BfAB \stackrel{f}{\to} A given we may send UxBU \stackrel{x}{\to} B to the composition

(UxBfA)=(Uf(x)A). (U \stackrel{x}{\to} B \stackrel{f}{\to}A ) = (U \stackrel{f(x)}{\to} A) \,.

A free variable becomes a bound variable after application of a quantifier: for instance the image of f:PXf\colon P \to X under base change

𝒞 /X𝒞 \mathcal{C}_{/X} \stackrel{\to}{\stackrel{\leftarrow}{\to}} \mathcal{C}

represents, for the left adjoint the type

x:X,P(x) \exists x\colon X , P(x)

(existential quantifier), and the the right adjoint the type

x:X,P(x) \forall x\colon X , P(x)

(universal quantifier) in which now xx is a bound variable.


A textbook account with an eye towards applications in computer science is in section 1.2 of

An exposition on the relation between free variables and universal quantification is in

  • Andrej Bauer, Free variables are not “implicitly universally quantified”! (web)

Last revised on March 26, 2023 at 13:27:47. See the history of this page for a list of all contributions to it.