|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-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|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, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
which is intended to be true if and only if is true for every possible element of .
Note that it is quite possible that may be provable (in a given context) for every term of type that can actually be constructed in that context yet cannot be proved. Therefore, we cannot define the quantifier by taking the idea literally and applying it to terms.
Let be an arbitrary context and a type in so that is extended by a free variable of type . We assume that we have a weakening? principle that allows us to interpret any proposition in as a proposition in . Fix a proposition in , which we think of as a predicate in with the free variable . Then the universal quantification of is any proposition in such that, given any proposition in , we have
It is then a theorem that the universal quantification of , 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 explicit by thinking of as a propositional function and writing instead; to go along with this one usually conflates and . Then the rule appears as follows:
In terms of semantics (as for example topos-theoretic semantics; see the next section), the weakening from to corresponds to pulling back along a product projection , where is the interpretation of the type , and is the interpretation of . In other words, if a statement read in context is interpreted as a subobject of , then the statement read in context is interpreted by pulling back along the projection, obtaining a subobject of .
As observed by Lawvere, we are not particularly constrained to product projections; we can pull back along any map . (Often we have a class of display maps and require to be one of these.) Alternatively, any pullback functor can be construed as pulling back along an object , i.e., along the unique map corresponding to an object in the slice , since we have the identification .
where is the functor that takes an object to the product projection , where is the dependent sum (i.e., forgetful functor taking to ) that is left adjoint to , and where is the dependent product operation that is right adjoint to .
to give universal quantification over the domain (or context) :
Dually, the extra left adjoint , obtained from the dependent sum 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 -truncated objects (= subterminal objects), whereas the dependent sum does not.)
This interpretation of universal quantification as the right adjoint to context extension is also used in the notion of hyperdoctrine.
Then the dependent product
is the set of sections of the bundle . 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.
and further developed in