nLab universal quantifier



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
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit 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 setinternal homfunction type
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian productdependent productdependent product type
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijectionisomorphism/adjoint equivalenceequivalence of types
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, the universal quantifier\forall” is the quantifier used to express, given a predicate ϕ\phi with a free variable xx of type TT, the proposition

x:T,ϕx, \forall\, x\colon T, \phi x \,,

which is intended to be true if and only if ϕa\phi a is true for every possible element aa of TT.

Note that it is quite possible that ϕa\phi a may be provable (in a given context) for every term aa of type TT that can actually be constructed in that context yet x:T,ϕx\forall x\colon T, \phi x cannot be proved. Therefore, we cannot define the quantifier by taking the idea literally and applying it to terms.


We work in a logic in which we are concerned with which propositions entail which propositions (in a given context); in particular, two propositions which entail each other are considered equivalent.

Let Γ\Gamma be an arbitrary context and TT a type in Γ\Gamma so that ΔΓ,x:T\Delta \coloneqq \Gamma, x\colon T is Γ\Gamma extended by a free variable xx of type TT. We assume that we have a weakening rule that allows us to interpret any proposition QQ in Γ\Gamma as a proposition Q[x^]Q[\hat{x}] in Δ\Delta. Fix a proposition PP in Δ\Delta, which we think of as a predicate in Γ\Gamma with the free variable xx. Then the universal quantification of PP is any proposition x:T,P\forall\, x\colon T, P in Γ\Gamma such that, given any proposition QQ in Γ\Gamma, we have

  • Q Γx:T,PQ \vdash_{\Gamma}\forall\, x\colon T, P if and only if Q[x^] Γ,x:TPQ[\hat{x}] \vdash_{\Gamma, x\colon T} P.

It is then a theorem that the universal quantification of PP, if it exists, is unique. The existence is typically asserted as an axiom in a particular logic, but this may be also be deduced from other principles (as in the topos-theoretic discussion below).

Often one makes the appearance of the free variable in PP explicit by thinking of PP as a propositional function and writing P(x)P(x) instead; to go along with this one usually conflates QQ and Q[x^]Q[\hat{x}]. Then the rule appears as follows:

  • Q Γx:T,P(x)Q \vdash_{\Gamma}\forall\, x\colon T, P(x) if and only if Q Γ,x:TP(x)Q \vdash_{\Gamma, x\colon T} P(x).

In terms of semantics (as for example topos-theoretic semantics; see the next section), the weakening from QQ to Q[x^]Q[\hat{x}] corresponds to pulling back along a product projection σ(T)×AA\sigma(T) \times A \to A, where σ(T)\sigma(T) is the interpretation of the type TT, and AA is the interpretation of Γ\Gamma. In other words, if a statement QQ read in context Γ\Gamma is interpreted as a subobject of AA, then the statement QQ read in context Δ=Γ,x:T\Delta = \Gamma, x \colon T is interpreted by pulling back along the projection, obtaining a subobject of σ(T)×A\sigma(T) \times A.

As observed by Lawvere, we are not particularly constrained to product projections; we can pull back along any map f:BAf \colon B \to A. (Often we have a class of display maps and require ff to be one of these.) Alternatively, any pullback functor f *:Set/ASet/Bf^\ast\colon Set/A \to Set/B can be construed as pulling back along an object X=(f:BA)X = (f \colon B \to A), i.e., along the unique map !:X1!\colon X \to 1 corresponding to an object XX in the slice Set/ASet/A, since we have the identification Set/B(Set/A)/XSet/B \simeq (Set/A)/X.

In topos theory / in terms of adjunctions

In terms of the internal logic in some ambient topos \mathcal{E},

Universal quantification is essentially the restriction of the direct image right adjoint of a canonical étale geometric morphism X *X_\ast,

/XX *X *X !, \mathcal{E}/X \stackrel{\overset{X_!}{\to}}{\stackrel{\overset{X^*}{\leftarrow}}{\underset{X_*}{\to}}} \mathcal{E} \,,

where X *X^\ast is the functor that takes an object AA to the product projection π:X×AX\pi \colon X \times A \to X, where X !=Σ XX_! = \Sigma_X is the dependent sum (i.e., forgetful functor taking f:AXf \colon A \to X to AA) that is left adjoint to X *X^\ast, and where X *=Π XX_\ast = \Pi_X is the dependent product operation that is right adjoint to X *X^\ast.

The dependent product operation restricts to propositions by pre- and postcomposition with the truncation adjunctions

τ 1τ 1 \tau_{\leq -1} \mathcal{E} \stackrel{\overset{\tau_{\leq -1}}{\leftarrow}}{\underset{}{\hookrightarrow}} \mathcal{E}

to give universal quantification over the domain (or context) XX:

/X X *X *X ! τ 1 τ 1 τ 1/X X X τ 1. \array{ \mathcal{E}/X & \stackrel{\overset{X_!}{\to}}{\stackrel{\overset{X^*}{\leftarrow}}{\underset{X_*}{\to}}} & \mathcal{E} \\ {}^\mathllap{\tau_{\leq_{-1}}}\downarrow \uparrow && {}^\mathllap{\tau_{\leq_{-1}}}\downarrow \uparrow \\ \tau_{\leq_{-1}} \mathcal{E}/X & \stackrel{\overset{\exists_X}{\to}}{\stackrel{\overset{}{\leftarrow}}{\underset{\forall_X}{\to}}} & \tau_{\leq_{-1}}\mathcal{E} } \,.

Dually, the extra left adjoint X\exists_X, obtained from the dependent sum X !X_! by pre- and post-composition with the truncation adjunctions, expresses the existential quantifier. (The situation with the universal quantifier is somewhat simpler than for the existential one, since the dependent product automatically preserves (1)(-1)-truncated objects (= subterminal objects), whereas the dependent sum does not.)

The same makes sense, verbatim, also in the (∞,1)-logic of any (∞,1)-topos.

This interpretation of universal quantification as the right adjoint to context extension is also used in the notion of hyperdoctrine.

In dependent type theory

In dependent type theory, the universal quantifier is the dependent product type of a family of h-propositions:

Formation rules for the universal quantifier:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ap(x):isProp(B(x))Γ(x:A).B(x)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isProp}(B(x))}{\Gamma \vdash \forall (x:A).B(x) \; \mathrm{type}}

Introduction rules for the universal quantifier:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ap(x):isProp(B(x))Γ,x:Ab(x):B(x)Γλ(x:A).b(x):(x:A).B(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isProp}(B(x)) \quad \Gamma, x:A \vdash b(x):B(x)}{\Gamma \vdash \lambda(x:A).b(x):\forall (x:A).B(x)}

Elimination rules for the universal quantifier:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ap(x):isProp(B(x))Γf:(x:A).B(x)Γa:AΓf(a):B[a/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isProp}(B(x)) \quad \Gamma \vdash f:\forall (x:A).B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash f(a):B[a/x]}

Computation rules for the universal quantifier:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ap(x):isProp(B(x))Γ,x:Ab(x):B(x)Γa:AΓβ :λ(x:A).b(x)(a)= B[a/x]b[a/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isProp}(B(x)) \quad \Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_\forall:\lambda(x:A).b(x)(a) =_{B[a/x]} b[a/x]}

Uniqueness rules for the universal quantifier:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ap(x):isProp(B(x))Γf:(x:A).B(x)Γη :f= (x:A).B(x)λ(x).f(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isProp}(B(x)) \quad \Gamma \vdash f:\forall (x:A).B(x)}{\Gamma \vdash \eta_\forall:f =_{\forall (x:A).B(x)} \lambda(x).f(x)}

The dependent product type of a family of h-propositions is always an h-proposition.

One doesn’t need all dependent product types to define universal quantifiers. The isProp types are definable without all dependent product types, by use of center of contraction, which are also definable without all dependent product types. This means that one could define the type-theoretic internal logic of a Heyting category or Boolean category which are not locally cartesian closed, for strongly predicative mathematics.


Let =\mathcal{E} = Set, let X=X = \mathbb{N} be the set of natural numbers and let ϕ2\phi \coloneqq 2\mathbb{N} \hookrightarrow \mathbb{N} be the subset of even natural numbers. This expresses the proposition ϕ(x)IsEven(x)\phi(x) \coloneqq IsEven(x).

Then the dependent product

(ϕSet/)( x:Xϕ(x)Set) (\phi \in Set/{\mathbb{N}}) \mapsto (\prod_{x\colon X} \phi(x) \in Set)

is the set of sections of the bundle 22 \mathbb{N} \hookrightarrow \mathbb{N}. But since over odd numbers the fiber of this bundle is the empty set, there is no possible value of such a section and hence the set of sections is itself the empty set, so the statement “all natural numbers are even” is, indeed, false.

\phantom{-}symbol\phantom{-}\phantom{-}in logic\phantom{-}
A\phantom{A}\inA\phantom{A}element relation
A\phantom{A}:\,:A\phantom{A}typing relation
A\phantom{A}\vdashA\phantom{A}A\phantom{A}entailment / sequentA\phantom{A}
A\phantom{A}\topA\phantom{A}A\phantom{A}true / topA\phantom{A}
A\phantom{A}\botA\phantom{A}A\phantom{A}false / bottomA\phantom{A}
A\phantom{A}\LeftrightarrowA\phantom{A}logical equivalence
A\phantom{A}\neqA\phantom{A}negation of equality / apartnessA\phantom{A}
A\phantom{A}\notinA\phantom{A}negation of element relation A\phantom{A}
A\phantom{A}¬¬\not \notA\phantom{A}negation of negationA\phantom{A}
A\phantom{A}\existsA\phantom{A}existential quantificationA\phantom{A}
A\phantom{A}\forallA\phantom{A}universal quantificationA\phantom{A}
A\phantom{A}\wedgeA\phantom{A}logical conjunction
A\phantom{A}\veeA\phantom{A}logical disjunction
symbolin type theory (propositions as types)
A\phantom{A}\toA\phantom{A}function type (implication)
A\phantom{A}×\timesA\phantom{A}product type (conjunction)
A\phantom{A}++A\phantom{A}sum type (disjunction)
A\phantom{A}00A\phantom{A}empty type (false)
A\phantom{A}11A\phantom{A}unit type (true)
A\phantom{A}==A\phantom{A}identity type (equality)
A\phantom{A}\simeqA\phantom{A}equivalence of types (logical equivalence)
A\phantom{A}\sumA\phantom{A}dependent sum type (existential quantifier)
A\phantom{A}\prodA\phantom{A}dependent product type (universal quantifier)
symbolin linear logic
A\phantom{A}\multimapA\phantom{A}A\phantom{A}linear implicationA\phantom{A}
A\phantom{A}\otimesA\phantom{A}A\phantom{A}multiplicative conjunctionA\phantom{A}
A\phantom{A}\oplusA\phantom{A}A\phantom{A}additive disjunctionA\phantom{A}
A\phantom{A}&\&A\phantom{A}A\phantom{A}additive conjunctionA\phantom{A}
A\phantom{A}\invampA\phantom{A}A\phantom{A}multiplicative disjunctionA\phantom{A}
A\phantom{A}!\;!A\phantom{A}A\phantom{A}exponential conjunctionA\phantom{A}


The observation that substitution forms an adjoint pair/adjoint triple with the existential/universal quantifiers is due to

and further developed in

  • William Lawvere, Equality in hyperdoctrines and

    comprehension schema as an adjoint functor_, Proceedings of the AMS Symposium on Pure Mathematics XVII (1970), 1-14.

Last revised on November 26, 2022 at 21:16:36. See the history of this page for a list of all contributions to it.