Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels





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 DD (such as a category of geometric shapes for higher structures), which satisfies certain properties or is equipped with certain structure. The category DD 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) SetSet-valued diagrams on some inverse category. If CC is an inverse category and xCx\in C an object, then xx represents one geometric shape appearing in the structures under consideration, while all of the morphisms out of xx 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 xx 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,

  • A FOLDS signature or vocabulary for dependent sorts (DSV) consists of a simple category together with a distinguished set of maximal objects, called the relation symbols. The objects that are not relation symbols are called kinds.




Last revised on December 11, 2018 at 20:57:01. See the history of this page for a list of all contributions to it.