nLab
3-theory

Context

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
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher 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

semantics

Higher algebra

Idea

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.

Examples

  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).

References

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