|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 at least one object of type .
Note that it is quite possible that may be provable (in a given context) yet cannot be proved for any term of type that can actually be constructed in that context. 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 rule 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 existential quantification of is any proposition in such that, given any proposition in , we have
It is then a theorem that the existential 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:
The categorical semantics of existential quantification is given by the (-1)-truncation of the dependent sum-construction along the projection morphism that projects out the free variable over which the existental quantifier quantifies.
Notice that the categorical semantics of the context extension from to corresponds to base change/pullback along the 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 .
(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 .
Therefore in terms of the internal logic of a suitable category (with sufficient pullbacks)
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 existential quantification over the domain (or context) :
Dually, the direct image functor (dependent product) expresses the universal quantifier. (In this case, it is somewhat simpler, since the dependent product automatically preserves -truncated objects; no additional truncation step is necessary.)
This interpretation of existential quantification as the left adjoint to context extension is also used in the notion of hyperdoctrine.
Then the dependent sum
Notice that before the -truncation the operation remembers not just that there is an even number, but it remembers “all proofs that there is one”, namely every example of an even number.
and further developed to the notion of hyperdoctrines in