Contents
Context
Type theory
Deduction and Induction
Constructivism, Realizability, Computability
Foundations
foundations
The basis of it all
-
mathematical logic
-
deduction system, natural deduction, sequent calculus, lambda-calculus, judgment
-
type theory, simple type theory, dependent type theory
-
collection, object, type, term, set, element
-
equality, judgmental equality, typal equality
-
universe, size issues
-
higher-order logic
Set theory
Foundational axioms
Removing axioms
Contents
Idea
Objective type theory is a dependent type theory without judgmental equality.
This means that in additon to being a weak type theory, where the computation and uniqueness rules (beta-reduction and eta-conversion) for each type in the type theory are all propositional computational and uniqueness rules using the identity type, objective type theory is similar to other non-type theory foundations such as the various flavors of set theory, since it also only has one notion of equality, propositional equality, and uses propositional equality in definitions.
Objective type theory has decidable type checking, and the type checking can be done in quadratic time.
Substitutions
There are two ways one could define substitutions in dependent type theory, either by explicit substitution or by showing that the substitution rule is an admissible rule. However, for objective type theory, only the latter approach is possible.
The problem with explicit substitutions is that with explicit substitution approaches, the contexts are usually formalized with judgmental equality of morphisms of contexts, such that the categorical semantics correspond to a functor from the category of contexts to the 2-category which takes a context to the slice category . However, without judgmental equality, doesn’t form a category anymore, since the morphisms in don’t form a set anymore, and one can no longer express the unit and associatvity laws for composition of morphisms of contexts, which are needed for the unit and associativity laws of explicit substitution. The same holds for explicit substitution via telescopes; here, substitutions are elements of telescopes, and one has judgmental equalities of the substitutions themselves.
Alternatively, one can try to define structure indicating that the collection of contexts forms an -category, avoiding the need for judgmental equality entirely, but one quickly runs into coherence issues, since the structure of an -category cannot be expressed from nothing using a finite amount of structure. This is similar to the issues in defining an -category in dependent type theory without using pre-existing simplicial or cubical structure or modalities. Thus, it is currently unknown how to avoid this use of judgmental equality for explicit substitution and/or telescopes in dependent type theory, rendering it impossible for those to formulate objective type theory.
The other approach involving an admissible substitution rule doesn’t suffer from this issue because the analogue in admissible substitution approaches of the judgmental equality in explicit substitution approaches resides in the metatheory rather than the actual theory itself, so the type theory itself can genuinely be said to not contain any judgmental equalities.
Definitions in objective type theory
In section 9 of Winterhalter2020, Theo Winterhalter indicates that there are many ways to formalize dependent type theory. One important aspect is whether to use Russell universes or a separate type judgment to denote types: van der Berg & den Besten 2021 and UPF 2013 both use Russell universes in their formal presentation of dependent type theory, while Rijke 2022 uses a separate type judgment to denote types.
In the context of objective type theory, there is no judgmental equality in the type theory in the traditional sense, so there is the question of how to define aliases of terms and types in the type theory. For the case of terms, that is easily resolved by using identity types. For example, to define as the successor of the succcessor of zero in the natural numbers type, one could postulate an identification . On the other hand, the situation for types is a bit more complicated. For example, the isContr modality in dependent type theory indicating whether the type is a contractible type is usually defined to be . But without judgmental equality, one cannot simply write
When presenting dependent type theory using Russell universes, the answer is as simple as that for terms: one simply uses typal equality instead, because every type is an element of a Russell universe, and so one could write
for types and . On the other hand, when using a separate type judgment, types are not elements of other types, and thus one cannot compare them for typal equality. Instead, one has to use equivalences of types instead:
This poses another problem: the equivalence type has not yet been defined yet.
When expanded out using dependent sum types and function types, one gets
UPF 2013 says that the type family comes with
This could be made into inference rules
Breaking the functions down, the inference rules become
One could postulate a single equality judgment between types which reflects into an equivalence:
A similar equality judgment could be made for terms, with a similar rule to reflect it into an identification:
These equalities, while judgmental, are different from the judgmental equality found in other dependent type theories like Martin-Löf type theory and cubical type theory in that they have neither the structural rules nor the congruence rules found in those theories: they are only a formalization of a notational representation of definitional equality and definitional equivalence otherwise represented by identity types and equivalence types.
Without a separate type judgment
In this section, we describe a formalization of objective type theory using an infinite hierarchy of Russell universes with cumulativity, in the style of UPF 2013.
Judgments, contexts, and universes
This presentation of objective type theory consists of the following judgments:
-
Element judgments, where we judge to be an element of ,
-
Context judgments, where we judge to be a context, .
In addition, we have a countably infinite number of inference rules for the countably infinite number of Russell universes in the theory, here represented by a natural numbers metavariable for conciseness:
as well as inference rules for either cumulativity, that any type in a universe is also in the next universe of the hierarchy, or lifting, that any type in a universe can be lifted to the next universe of the hierarchy:
Contexts are lists of element judgments , , , et cetera, and are formalized by the inference rules for the empty context and extending the context by a element judgment
Variable rule
There is one additional structural rule in objective type theory, the variable rule.
The variable rule states that we may derive a element judgment if the element judgment is in the context already:
Admissible structural rules
The weakening rule and the substitution rule are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations.
Let be any arbitrary judgment. Then the weakening rule is
and the substitution rule is
Families of types and elements
A family of elements is an element in the context of the variable judgment , . They are usually written as to indicate its dependence upon . Given a particular element , the element is an element dependent upon .
Since types are elements of universe, a family of types is simply a family of elements of universes.
Identity types
Formation rules for identity types:
Introduction rules for identity types:
Elimination rule for identity types:
Computation rules for identity types:
Definitions
Definitions of a symbol for the element are made by using identity types between the symbol and element: . Definitions of a symbol for the type are made in the same way, as . Thus, the identity type behaves very similarly to explicit conversion as discussed in section 9.2 of Winterhalter2020.
Dependent function types
Formation rules for dependent function types:
Introduction rules for dependent function types:
Elimination rules for dependent function types:
Computation rules for dependent function types
Uniqueness rules for dependent function types:
Function types
Formation rules for function types:
Introduction rules for function types:
Elimination rules for function types:
Computation rules for function types
Uniqueness rules for function types:
Pair types
Formation rules for pair types:
Introduction rules for pair types:
Elimination rules for pair types:
Computation rules for pair types:
Uniqueness rules for pair types:
Dependent pair types
Formation rules for dependent pair types:
Introduction rules for dependent pair types:
Elimination rules for dependent pair types:
Computation rules for dependent pair types:
Uniqueness rules for dependent pair types:
isContr, uniqueness quantifiers, isEquiv, and equivalence types
Now that we have identity types, dependent sum types, and dependent product types, we can use that to define
Univalence
The univalence axiom states that the identity type between two types of a universe is equivalent to the equivalence type between said types:
Positive types
Now that we have the uniqueness quantifier we can combine the elimination rule, the computation rule, and the uniqueness rule for any positive type into one rule, the induction rule.
Unit type
Formation rules for the unit type:
Introduction rules for the unit type:
Induction rule for the unit type:
Empty type
Formation rules for the empty type:
Induction rule for the empty type:
Booleans type
Formation rules for the booleans type:
Introduction rules for the booleans type:
Induction rule for the booleans type:
Natural numbers type
Formation rules for the natural numbers type:
Introduction rules for the natural numbers type:
Induction rule for the natural numbers type:
Integers type
Formation rules for the integers type:
Introduction rules for the integers type:
Induction rule for the integers type:
With a separate type judgment
In this section, we describe a formalization of objective type theory using a type judgment, in the style of Rijke 2022.
Judgments and contexts
This presentation of objective type theory consists of the following judgments:
-
Type judgments, where we judge to be a type,
-
Element judgments, where we judge to be an element of ,
-
Context judgments, where we judge to be a context, .
Contexts are lists of element judgments , , , et cetera, and are formalized by the rules for the empty context and extending the context by a element judgment
Variable rule
There is one additional structural rule in objective type theory, the variable rule.
The variable rule states that we may derive a element judgment if the element judgment is in the context already:
Admissible structural rules
The weakening rule and the substitution rule are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations.
Let be any arbitrary judgment. Then the weakening rule is
and the substitution rule is
Families of types and elements
A family of types is a type in the context of the element judgment , , they are usually written as to indicate its dependence upon . Given a particular element , the type is a type dependent upon .
A family of terms is a term in the context of the variable judgment , . They are likewise usually written as to indicate its dependence upon . Given a particular element , the element is an element dependent upon .
Identity types
Formation rules for identity types:
Introduction rules for identity types:
Elimination rule for identity types:
Computation rules for identity types:
Dependent function types
Formation rules for dependent function types:
Introduction rules for dependent function types:
Elimination rules for dependent function types:
Computation rules for dependent function types
Uniqueness rules for dependent function types:
Equivalence types
Formation rules for equivalence types:
Introduction rules for equivalence types:
Elimination rules for equivalence types:
Computation rules for equivalence types:
Uniqueness rules for equivalence types:
Definitions
Definitions of a symbol for the element are made by using identity types between the symbol and element: . Definitions of a symbol for the type are made by using equivalence types between the symbol and the type: .
Function types
Formation rules for function types:
Introduction rules for function types:
Elimination rules for function types:
Computation rules for function types
Uniqueness rules for function types:
Pair types
Formation rules for pair types:
Introduction rules for pair types:
Elimination rules for pair types:
Computation rules for pair types:
Uniqueness rules for pair types:
Dependent pair types
Formation rules for dependent pair types:
Introduction rules for dependent pair types:
Elimination rules for dependent pair types:
Computation rules for dependent pair types:
Uniqueness rules for dependent pair types:
isContr and uniqueness quantifiers
Now that we have equivalence types, identity types, dependent sum types, and dependent product types, we can use that to define
Positive types
Now that we have the uniqueness quantifier we can combine the elimination rule, the computation rule, and the uniqueness rule for any positive type into one rule, the induction rule.
Empty type
Formation rules for the empty type:
Recursion rule for the empty type:
Induction rule for the empty type:
Unit type
Formation rules for the unit type:
Introduction rules for the unit type:
Recursion rule for the unit type:
Induction rule for the unit type:
Booleans type
Formation rules for the booleans type:
Introduction rules for the booleans type:
Recursion rule for the booleans type:
Induction rule for the booleans type:
Natural numbers type
Formation rules for the natural numbers type:
Introduction rules for the natural numbers type:
Recursion rule for the natural numbers type:
Induction rule for the natural numbers type:
Integers type
Formation rules for the integers type:
Introduction rules for the integers type:
Recursion rule for the integers type:
Induction rule for the integers type:
Categorical semantics
The fragment of objective type theory consisting of only identity types and dependent product types can be interpreted in any path category with weak homotopy -types.
See also
References
The original paper on this topic:
General dependent type theory references used for the formalizations of objective type theory in this article: