|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|
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 inhabitation is the simpler notion, which emptiness is defined as the negation of.
The term ‘inhabited’ 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, and write to mean that is inhabited. The latter we can interpret literally if we regard as a reference to an inequality relation other than the denial inequality, such as the inequality defined for subsets by . If we prefer to reserve for the denial inequality, then we can write for this stronger inequality of sets (although it is not an apartness relation), and hence to mean that is inhabited.
In type theory there are two possible notions of inhabited type: a type whose propositional truncation has an element (or term), or a type that itself has an element (or term). The former is what corresponds to the above notion of inhabitedness in set theory, since is the propositions as types interpretation of . The latter is more like the notion of a pointed set.
The assertion is a mildly nonconstructive logical principle called the propositional axiom of choice?. It follows from excluded middle, but in the internal logics of some toposes, it can fail, so that these two notions of “inhabited type” really are different.
An inhabited set is the special case of an internally inhabited object in the topos Set. The two notions of inhabited type correspond to internally and externally inhabited objects (which are, respectively, those objects where is an epimorphism, and those which admit a global element ).