|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|
What is called FOLDS (for: first-order logic with dependent sorts) is a form of (intuitionistic or classical) predicate logic with a weak form of equality, in which category theory (and even higher category theory) can be formulated but it is impossible to violate, say, the mathematical principle of equivalence. It also induces general notions of equivalence for higher structures and for objects in higher structures, which reduce to familiar notions in most or all cases.
Formally speaking, FOLDS is “merely” a “first-order fragment” of dependent type theory, but its special treatment of equality, its notions of equivalence, and its relationship to higher-categorical structures distinguish it from DTT in general. These aspects have been developed primarily by Michael Makkai.
FOLDS can be formulated using dependent types, terms, contexts, and judgments, as is typical in type theory. However, it is perhaps easier for a category theorist to understand when presented as the study of the presheaves which underlie higher-categorical structures.
Both algebraic and geometric definitions of higher-categorical structures are generally specified by giving a presheaf on some small category (such as a category of geometric shapes for higher structures), which satisfies certain properties or is equipped with certain structure. The category in question is usually a Reedy category, and as such comes equipped with a stratification of its objects by “degree,” and a division of its morphisms into “coface maps,” which raise degree, and “codegeneracy maps,” which lower degree. The perspective of FOLDS is that actually the codegeneracy maps should be regarded as part of the structure imposed (when present, they usually assign “identities”), while the coface maps are what really describe the “geometric shape” or “dependency structure.” Note that in some cases, such as opetopic sets and globular sets, there are no degeneracies to start with.
This suggests that FOLDS should study presheaves on some direct category, or equivalently (changing the variance) -valued diagrams on some inverse category. If is an inverse category and an object, then represents one geometric shape appearing in the structures under consideration, while all of the morphisms out of indicate the lower-dimensional “faces” of such a shape, i.e. the “boundary” which it fills. However, for an arbitrary inverse category, a given shape can still have infinitely many faces in its boundary; this is difficult to deal with in logic, so we impose the extra requirement that the category have finite fan-out: every object is the source of only finitely many arrows altogether. A category with finite fan-out is an inverse category iff it is also both skeletal and one-way (every endomorphism is an identity); thus we study skeletal one-way categories with finite fan-out. In FOLDS these are called simple categories.
A FOLDS signature, or vocabulary, should then consist of a simple category of kinds, together with information about function and relation symbols. However, it turns out to be easier to include only relation symbols; the values of functions can then be recovered as the unique objects satisfying some relation, or more generally as unique-up-to-equivalence objects equipped with some higher structure (cf. anafunctor, for instance). One reason relation symbols are easier is that they can be represented simply as additional “shapes,” whose boundary consists of those elements which they relate. Such a shape should be maximal, in the sense that it is not the target of any nonidentity arrow. Thus,