nLab two-level type theory

Contents

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
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

semantics

Deduction and Induction

Constructivism, Realizability, Computability

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

Idea

Two-level type theory (2LTT) refers to versions of Martin-Lof type theory that combine two type theories: one level as a homotopy type theory, which may include univalent universes and higher inductive types, and the second level as a traditional form of type theory validating uniqueness of identity proofs. The second layer may be understood as the internalised meta-theory of the first.

The rules are much inspired by the homotopical semantics in fibration categories and model categories, according to which the types of the homotopy layer are sometimes called fibrant types and the others non-fibrant types. An alternative terminology is simply types (since these are the objects of real interest) and pretypes (an auxiliary structure used to study the types).

In other words, where default homotopy type theory has categorical semantics (see at relation between category theory and type theory) in suitable type-theoretic model categories but in such a way that only the (infinity,1)-category presented by that really matters, in two-level type theory one adds explicit control over the presenting model category (or other kind of fibration category), thus apparently breaking the (,1)(\infty,1)-categorical “principle of equivalence” but providing more tools for handling the presentation. It is an open question to what extent the principle of equivalence is actually broken, i.e. whether results proven in two-level type theory can be transferred to any model categorical presentation.

Type theories

  • The first proposal for two-level type theory was Vladimir Voevodsky‘s Homotopy Type System. This system had a reflection rule collapsing the non-fibrant “exact equality” to judgmental equality, making some things easier but making type-checking undecidable.

  • More recently the proposals of ACK simply assumes uniqueness of identity proofs for the exact equality; this seems to suffice for most if not all purposes.

  • Computationalcubical type theory can also include a non-fibrant layer: its syntax is interpreted as cubical sets, where “fibrancy” is a defined condition on pretypes (existence of Kan operations).

Applications

Semisimplicial types

Two-level type theories (including HTS and ACK) were motivated to a large extent by the technical difficulties encountered in formalizing semisimplicial types in default homotopy type theory (HoTT). This problem comes precisely from the fact that HoTT is really the internal language of some (infinity,1)-topos and hence defining simplicial objects or similar here means to speak of simplicial objects in an (infinity,1)-category, which means that the simplicial identities hold only up to coherent higher homotopy. The problem of syntactically encoding the infinite amount of this coherence data remains unsolved to date. For semisimplicial types the difficulties greatly reduce (since the evident iterated dependent type-definition of a semisimplicial type is automatically interpreted by a Reedy-fibrant object in the given type-theoretic model category, which takes care of all the homotopy coherence by the power of model category theory, see at internal (infinity,1)-category for more on this) but technical problems remain even in formulating the plain 1-categorical simplicial identities to all degrees.

The “exact equality” of two-level type theories solves this problem because such equalities can be defined by induction.

Variations

Natural numbers

One important choice to be made in writing down a two-level type theory is whether there is one natural numbers type or two. There must certainly be a fibrant natural numbers type; the question is whether the elimination rule for this “fibrant nat” allows elimination also into non-fibrant types. If it does not, then there should also be a “non-fibrant nat” which is not fibrant, but whose elimination principle can eliminate into other non-fibrant types.

Semantically, this distinction corresponds to whether the natural numbers object of the model category presentation is already fibrant, or whether it needs to be fibrantly replaced to represent a (fibrant) type. In some models, such as simplicial sets, it is already fibrant; but in others, such as local model structure on simplicial presheaves, it is not. It is an open question whether any (infinity,1)-topos can be presented by a model category in which the natural numbers object is fibrant, and thus serve as semantics for a two-level type theory with only one natural numbers type.

Since the definition of semisimplicial types requires an inductive definition of a (non-fibrant) exact equality, if there are two nats then it must use the non-fibrant one. This means that, without additional rules, a two-level type theory with two nats cannot define a fibrant type of untruncated semisimplicial types: for each non-fibrant nn it can define a fibrant type of nn-truncated semisimplicial types, but the limit of these types over the non-fibrant nat is no longer fibrant. Assuming only one nat is sufficient to solve this problem, but as mentioned above this may exclude desirable models. Another weaker axiom, which is satisfied in all sufficiently nice model categories, is that fibrant types are closed under limits of towers of fibrations indexed by the non-fibrant nat. (In two-level type theory terminology, this is a strengthening of the assumption that the non-fibrant nat is “cofibrant”.)

See also

References

  • Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus, Extending Homotopy Type Theory with Strict Equality, (arXiv:1604.03799)

  • Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler, Two-Level Type Theory and Applications, (arXiv:1705.03307)

Last revised on February 23, 2024 at 20:29:05. See the history of this page for a list of all contributions to it.