nLab set-level type 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




A type theory where types behave like sets, i.e. in which all types are h-sets. Thus, it is a form of set-level foundations. This includes:

Set-level type theory contrasts with higher-level type theory such as homotopy type theory or plain intensional type theory, where types behave (at least potentially) like n-groupoids or even infinity-groupoids. In the other direction, it contrasts with type theories where types behave like propositions (type theories of this sort are often called logics).

Set-level intensional type theories

In a set-level but intensional type theory, we distinguish definitional and propositional equality (unlike in extensional type theory), but no two terms can be propositionally equal in more than one way (up to propositional equality). In the language of homotopy type theory, this means that all types are h-sets. There are a number of equivalent ways to force this to be true by adding axioms to type theory.

  1. We can add as an axiom the “uniqueness of identity proofs” (axiom UIP) property that any two inhabitants of the same identity type Id A(x,y)Id_A(x,y) are themselves equal (in the corresponding higher identity type).

  2. We can add Streicher’s axiom K which says that any inhabitant of a self-equality type Id A(x,x)Id_A(x,x) is (propositionally) equal to the identity/reflexivity equality 1 x1_x. (Axiom K is so named because KK comes after JJ, and JJ usually denotes the eliminator for identity types.)

  3. In the presence of dependent sum types, we can add an axiom saying that if (a,b 1)(a,b_1) and (a,b 2)(a,b_2) are pairs in a dependent sum x:AB(x)\sum_{x\colon A} B(x) with the same first component, and the identity type Id x:AB(x)((a,b 1),(a,b 2))Id_{\sum_{x\colon A} B(x)}((a,b_1), (a,b_2)) is inhabited, then so is Id B(a)(b 1,b 2)Id_{B(a)}(b_1,b_2).

  4. We can allow definition of functions by a strong form of pattern matching, as in unmodified Agda. The relevant “extra strength” is to allow output types of a pattern match which are only well-defined after the pattern has been matched.

  5. In cubical type theory (with glue types? removed, since univalence is incompatible with set-level-ness), we can add a boundary separation rule, leading to XTT.

See also

Last revised on September 22, 2022 at 16:48:24. See the history of this page for a list of all contributions to it.