nLab 3-theory


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


Higher algebra


In the context of an account of logic described in terms of nn-theories (Shulman 18a), a 3-theory specifies a kind of 2-category. It does so by prescribing the allowable judgment structures of the 2-theories that can be expressed within it.


  1. The 3-theory of (totally unstructured) 2-categories. Syntactically, this corresponds to “unary type (2-)theories” with judgments such as x:Ab:Bx:A \vdash b:B with exactly one type to both the left and the right of the turnstile (LS 15).

  2. The 3-theory of cartesian monoidal 2-categories (or cartesian 2-multicategories). Syntactically, this corresponds to “simple type (2-)theories” with judgments such as x:A,y:B,z:Cd:Dx:A, y:B, z:C \vdash d:D with a finite list of types to the left but exactly one type to the right, and no dependent types (LSR 17).

  3. The 3-theory of first-order logic. Syntactically, this corresponds to type 2-theories with one layer of dependency: there is one layer of types which cannot depend on anything, and then there is a second layer of types (“propositions” in the logical reading) which can depend on types in the first layer, but not on each other. 2-theories here are for hyperdoctrines and indexed monoidal categories, and include (typed) first-order classical logic, first-order intuitionistic logic, first-order linear logic, the type theory of indexed monoidal categories, first-order modal logic, etc. Semantic 2-theories in this 3-theory should be a sort of “2-hyperdoctrine”. A higher-order logic is a 2-theory which adds rules specifying a universe of propositions.

  4. The 3-theory that corresponds syntactically to “dependent type (2-)theories” with judgments such as x:A,y:B(x),z:C(x,y)d:D(x,y,z)x:A, y:B(x), z:C(x, y) \vdash d:D(x, y, z). The semantic version of this should be some kind of “comprehension 2-category” (Shulman 18b). Homotopy type theory is a 2-theory defined in this 3-theory.

  5. The 3-theory that corresponds syntactically to “classical simple type (2-)theories” with judgments such as A,B,CD,EA,B,C \vdash D,E that allow finite lists of types on both sides of the turnstile. For instance, the 2-theory of *\ast-autonomous categories (classical linear logic), and also of Boolean algebras (classical nonlinear logic), live in this 3-theory, as does the 2-theory for symmetric monoidal categories described in (Shulman 19). Variants would allow composition along multiple types at once (corresponding to a prop), composition only along one type at a time (corresponding to a polycategory), or both.

  6. The classical 3-theory that extends the first-order 3-theory by allowing multiple sequents. (The term ‘classical’ here and above owes its origin to the contrast between systems LK and LJ of Gentzen's sequent calculus, where LJ provides a proof system for intuitionistic logic via restriction to single sequents of the rules of LK for classical logic. This naming practice leads to a certain confusion as it is quite possible to represent classical first-order logic in a single sequent system such as Gentzen’s NJ.)

A 3-theory may be said to subsume another 3-theory, in the sense that a 2-theory written in the latter may be formulated in the former. Here the first four 3-theories are ordered in terms of increasing expressivity. (5) subsumes (2), and (6) subsumes (3), but (4) and (5) are not comparable.

Modal variants of 2-theories may be defined in 3-theories where the types appearing in judgments are indexed by a system (2-category) of modes (Shulman 18b).


Last revised on September 15, 2020 at 08:49:32. See the history of this page for a list of all contributions to it.