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

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
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




The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms



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 January 25, 2023 at 19:31:32. See the history of this page for a list of all contributions to it.