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




In logic and type theory, the context of a judgement (or hypothetical judgement, with dependence on the context) consists of all of the assumptions that are made when that assertion is claimed to be valid; whether an assertion is in fact valid (or even meaningful) may depend on the context. The precise definition depends on the theory (or doctrine) that one is working in.

Generally, a context is thought of as relative to some underlying logical theory. This underlying theory will contain most of the assumptions of what constitutes validity; the context of an assertion in this theory will then include only those extra assumptions that may be used by that assertion. On the other hand, one could also think of the entire base theory as part of the context.


Theory of a group

In the theory of a group, it is understood that there is a group GG, that GG has various elements, that two elements of GG may be equal, that any two elements of GG have as product an element of GG, and that various equational laws are satisfied (which we will not list here). That is all taken for granted when discussing a group. However, the validity and meaningfulness of an assertion that two elements of GG commute will depend on (the rest of) the context.

To be more explicit, the assertion that aa and bb commute does not make sense without the additional context that aa and bb are elements of GG. Even in that context, this assertion, while at least meaningful, is not valid. However, if we add to the context the assumption that (ab) 2=a 2b 2(a b)^2 = a^2 b^2, then the assertion is valid. Written symbolically,

ab=ba \vdash\; a b = b a

is meaningless;

a:G,b:Gab=ba a\colon G,\; b\colon G \;\vdash\; a b = b a

is meaningful but invalid; and

(1)a:G,b:G,(ab) 2=a 2b 2ab=ba a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2 \;\vdash\; a b = b a

is valid.

In a sufficiently rich logical language, contexts are unnecessary, which is why contexts are not usually explained in accounts of logic for ordinary reasoning (including in ordinary mathematics). For example, the two meaningful assertions above may be rewritten thus:

(a:G),(b:G),ab=ba \vdash\; \forall (a\colon G),\; \forall (b\colon G),\; a b = b a


(a:G),(b:G),(ab) 2=a 2b 2ab=ba \vdash\; \forall (a\colon G),\; \forall (b\colon G),\; (a b)^2 = a^2 b^2 \;\Rightarrow\; a b = b a

Here the context on the left side is the empty context, consisting of no assumptions whatsoever (beyond those underlying the base theory).

However, these versions involve \forall and \Rightarrow, while the previous versions work in weaker logics. In fact, these assertions make sense (and the valid one may be proved) in the internal logic of a group object in a finitely complete category (and somewhat more generally than that). Accordingly, they can be interpreted as statements about any group object in any finitely complete category (and the valid one will then be interpreted as a true statement), exactly as they do for groups (which are group objects in the finitely complete category Set).

Even if one is completely uninterested in internalization or weak logics, a basic familiarity with contexts may help drive home a point that is important throughout reasoning: What you can state and prove depends on your assumptions.


Category of contexts

The category of contexts in a theory forms its syntactic category, which is a split model of type theory and is important in the relation between type theory and category theory. See Categorical semantics below.

Categorical semantics

The categorical semantics of a context Γ\Gamma in type theory is as the slice category 𝒞 /[Γ]\mathcal{C}_{/[\Gamma]} over the object that interprets Γ\Gamma. See at categorical semantics – Definition – Of dependent type theory – Contexts and type judgements.


A comprehensive definition of categorical semantics of contexts in homotopy type theory in type-theoretic model categories is in section 2 of