|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|
At least assuming classical logic, this is the same thing as a set that is not empty. Usually inhabited sets are simply called ‘non-empty’, but the positive word ‘inhabited’ reminds us that this is the simpler notion, which emptiness is defined as the negation of.
The terms ‘inhabited’ and ‘occupied’ come from constructive mathematics. In constructive mathematics (such as the internal logic of some topos or generally in type theory), a set/type that is not empty is not already necessarily inhabited. This is because double negation is nontrivial in intuitionistic logic. All the same, many constructive mathematicians use the old word ‘non-empty’ with the understanding that it really means inhabited.
In topos theory, one should distinguish two notions of “inhabited”. An object is internally inhabited if the unique morphism to a terminal object is an epimorphism. It is externally inhabited if there exists a global element, i.e., a morphism ; such forces to be a retraction and hence epic, i.e., forces to be internally inhabited. The two notions coincide if the terminal object is projective.
A generally useful principle in formulating appropriate categorical properties of Set is that external and internal notions should coincide. A general default understanding across the nLab is that is a well-pointed topos whose terminal object is projective and indecomposable. These latter properties of the terminal object hold for any well-pointed topos if the metalogic is classical; for purposes of constructive mathematics, we usually agree to add them in. In any event, we present a constructive/intuitionistic proof of the following result.
In a well-pointed topos, an object which is not internally inhabited is empty (is an initial object).
Note that the negation “not” in this statement is an external one, which is what makes it nontrivial. If an object is internally “not inhabited”, then it is empty essentially by definition.
Let be the epi-mono factorization of the unique map . Here is monic but not epic if is not epic, and we use this to prove . In that case, we have a map , whence since in a topos initial objects are strict. (For given , the projection has a section, and it follows that since and retracts of initial objects are initial. This also implies that for any the map is monic: for it is obviously true that for any pair of maps we have that implies , as is initial by strictness and this makes automatic.)
Let be the classifying map of the mono , and let be the classifying map of the mono . There is no map , else would retract it and hence be epic. Hence it is vacuously true that for all , and so by well-pointedness. Hence the subobjects and coincide, forcing . (In other words, the presence of a subobject classifier causes any generator to be a strong generator.)