|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|
|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|
consisting precisely of those elements of for which holds:
Note that is a subset of .
It is important to specify what language can be written in. This connects the axiom to logic and the foundations of mathematics. Arguably, first-order logic developed in order to explain the meaning of Ernst Zermelo's axiom of separation (although Zermelo himself disagreed with the interpretation that this gave). Separation is (usually) given as an axiom scheme because there is one axiom for each way to state a property in the language. (We also allow parameters in .)
From weaker to stronger:
For bounded separation aka restricted separation aka -separation, must be written in the language of first-order set theory and all quantifications must be guarded by a set: of the form or for some set .
For limited separation aka -separation, must be written in the language of first-order set theory and all quantifications must be guarded by a set or a power class: of the form , , etc. Limited separation trivially implies bounded separation, while bounded separation implies limited separation if power sets exist.
For full separation aka simply separation, must be written in the language of first-order set theory, but otherwise anything goes; in a class theory?, must be guarded by a class. Full separation trivially implies limited separation.
For large separation, must be written in the language of first-order class theory; of course, this only makes sense in a class theory. The difference in strength between the class theories and is precisely that the former has large separation but the latter does not.
Separation is sometimes called restricted comprehension; for full comprehension aka simply comprehension, no set needs to be given ahead of time. Full comprehension was proposed by Gottlob Frege, but leads to Russell's paradox. However, full comprehension can sometimes be allowed if the ambient logic is nonclassical, such as linear logic or paraconsistent logic.
For stratified comprehension, no set is given, but is restricted to stratified formulas, in which each variable can be given a consistent natural number (its stratification) such that appears in the formula only if . This is used in Van Quine?'s New Foundations.
Set theory is usually given in material form, with a language based on a global membership relation , and we have implicitly followed this above. However, separation makes sense also in structural set theory (although full comprehension does not, except in a structural class theory with a class of all sets?, where it again leads to paradox). The conclusion of the axiom is the existence of a set
and an injection such that
Note that , equipped with , is a subset of in the structural sense.
The structural axioms can of course be stated even in a material set theory, where they are actually weaker than the corresponding material axioms; however, the material axioms follow (as usual) from the structural axioms using restricted replacement, which is quite weak (and also follows from the material form of bounded separation).
If a structural set theory is given by stating axioms for the category of sets, then restricted separation amounts to the property that this category is a Heyting category. If it is an elementary topos, then since it satisfies the power set axiom, this implies limited separation as well. Full separation is somewhat less natural to state category-theoretically, but the combination of full separation with the structural axiom of collection is equivalent to saying that the category of sets is autological?.
Let be a bifibration over the category , and assume that each fibre of has a terminal object . For any morphism in , define the image of to be the pushforward (dependent sum) . This gives rise to a functor for each . Then is said to have comprehension, or to satisfy the comprehension schema, if each image functor has a right adjoint .
This means that for each there is a morphism in such that there is a bijection between commuting triangles in and morphisms in . Lawvere calls the morphism the extension of , so that one could say that satisfies the comprehension schema if the extensions of all predicates exist.
Notice that, in the above situation, morphisms in are in bijection with morphisms in , and that these are the same as morphisms in the total category that lie over . This leads to an alternative formulation of the definition, originally considered by Ehrhard 1988 (see also Jacobs 1993, Jacobs 99). If the fibres have terminal objects, then there is a (fully faithful) functor that sends to , and this is in fact right adjoint to the projection . Comprehension in the sense above is equivalent to the existence of a further right adjoint to this terminal-object functor (and in fact this version does not require pushforwards in ).
The implication from Lawvere’s definition to Ehrhard’s is clear. Conversely, if a fibration satisfies the Ehrhard definition, then there is a bijection between morphisms in and morphisms in . One must then show that the composite of this last with the canonical (given by applied to the counit ) is equal to applied to the morphism , thus giving a morphism in of the right sort. But in fact the morphism is unique with the property that applying the functor and composing with the counit gives the morphism , by the counit’s universal property, and applying to this commuting triangle in produces the required one in .
The tautological example which is useful to see what the abstract definition by Lawvere axiomatizes is the following.
Let Set be the category of sets and for a set let be the poset of subsets of , regarded as the propositions about elements in . Then comprehension exists and is given by sending a subset of regarded as an object of (hence regarded as a proposition) to the same subset, but now regarded as a monomorphism in Set into .
More generally, the same construction works for the posets of subobjects in any regular category.
There is a functor , from the large 1-category of categories and functors to the ‘very large’ 1-category of large categories and functors, that sends a category to the category of presheaves on , and a functor to the pullback functor . These pullback functors have left and right adjoints given by Kan extension.
If the hyperdoctrine has linear type theories/symmetric monoidal categories as fibers, then it is more natural to consider in def. 1 not the terminal object in some fiber (if any) but the tensor unit (which of course happens to be the terminal object in the case of cartesian monoidal) fibers.
In this case then the image functor in def. 1 is
is (the dependent version of) the canonical categorical interpretation of the !-modality of linear logic. See at dependent linear type theory – The canonical co-modality for more.
If the extension functors are fully faithful, then together they make into a ‘fibrewise reflective’ subfibration of the codomain fibration of , which is a reflective subfibration if the image functors preserve pullbacks. (See stable factorization system.)
Call a morphism of the form a subtype inclusion. Every morphism of factors through one such by means of the unit of the adjunction :
This gives rise to an orthogonal factorization system precisely when each is orthogonal to all subtype inclusions. It is shown by (Carboni et. al., section 2.12) that this holds if and only if subtype inclusions are closed under composition.
For the subobject fibration of a regular category, this gives the usual (regular epi, mono) factorization system, while for the fibration of presheaves over it gives the factorization of a functor into a final functor followed by a discrete fibration. (See also comprehensive factorization for a description of the latter as a factorization system in a 2-category.)
Although usually presented as an axiom scheme, in many cases, all instances of separation follow from finitely many special cases (which can then be packaged into a single axiom, using conjunction, although this is probably pointless). This is the case, for example, in ETCS (a structural set theory that satisfied bounded separation) and NBG (a material class theory that satisfies full separation). In type-theoretic foundations of mathematics, separation is usually invisible, but again some form (generally only bounded) can again be proved from a few specific axioms or constructions.
Full separation follows from the axiom of replacement and the principle of excluded middle (along with the axiom of the empty set). Therefore, the axiom is often left out entirely of a description of ZFC (the usually accepted foundation of mathematics). In versions of set theory for constructive mathematics, however, we often have replacement but only bounded or limited separation, and in any case separation must be listed explicitly.
Finn Lawler, section “Tabulation and comprehension” in Fibrations of predicates and bicategories of relations (2014)
Carboni, Janelidze, Kelly, Paré. On localization and stabilization for factorization systems. Applied Categorical Structures, 1997.
Full comprehension (a.k.a. “naive set theory”) in the context of logic without the contraction rule is discussed in:
Grishin, V. N., “Predicate and set theoretic calculi based on logic without contraction rules” (Russian), Izvestiya Akademii Nauk SSSR Seriya Matematicheskaya, 45(1): 47 – 68, 1981. English translation in Math. USSR Izv., 18(1): 41 – 59, 1982. (math-net.ru)
Kazushige Terui, Light Affine Set Theory: A Naive Set Theory of Polynomial Time, Studia Logica: An International Journal for Symbolic Logic, Vol. 77, No. 1 (Jun., 2004), pp. 9-40. (jstor) (pdf). See also Terui’s slides, Linear Logic and Naive Set Theory (Make our garden grow)