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 the computation and uniqueness rules (beta-reduction and eta-conversion) for each type in the type theory are all typal computational and uniqueness rules using the identity type, and in particular means that the identity type has to be introduced at the same time the dependent function type is introduced. As a result, the results in objective type theory are more general than in models which use judgmental equality for computational and uniqueness rules, since judgmental equality implies typal equality, while the converse isn’t necessarily the case.
In addition, 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.
Syntax
Judgments and contexts
Objective type theory consists of the following judgments:
-
Type judgments, where we judge to be a type,
-
Type definition judgments, where we judge to be defined as the type ,
-
Element judgments, where we judge to be an element of ,
-
Element definition judgments, where we judge to be defined as the term ,
-
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
Note that type and element definition judgments are not judgmental equalities; the former are single assignment operators while the latter are equivalence relations.
Structural rules
There are three structural rules in objective type theory, the variable rule?, the weakening rule, and the substitution rule.
The variable rule states that we may derive a element judgment if the element judgment is in the context already:
Let be any arbitrary judgment. Then we have the following rules:
The weakening rule:
The substitution rule:
The weakening and substitution rules 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.
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 .
In this section, we give the rules for the basic type formers of type theory, which are identification types and dependent function types.
Formation rules for identification types:
Formation rules for dependent function types:
Introduction rules for identification types:
Introduction rules for dependent function types:
Elimination rule for identification types:
Elimination rules for dependent function types:
Computation rules for identification types:
Computation rules for dependent function types
Optional Uniqueness rules for identification 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:
Heterogeneous identification types
Now that we have identification types and dependent product types, we can define heterogeneous identification types, which are important for defining the isEquiv dependent type on a function, used to determine whether a function is an equivalence, and then used to define definitions.
Formation rule for heterogeneous identification types:
Introduction rule for heterogeneous identification types:
Elimination rule for heterogeneous identification types:
Computation rules for heterogeneous identification types:
Function extensionality
Function extensionality states that given functions and the dependent function type
behaves as an identity system.
Dependent heterogeneous identification types
Now that we have identification types and dependent product types, we can define dependent heterogeneous identification types, which are important for defining the rules for higher inductive types.
Formation rule for dependent heterogeneous identification types:
Introduction rule for dependent heterogeneous identification types:
Elimination rule for dependent heterogeneous identification types:
Computation rules for dependent heterogeneous identification 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:
Structural rules for definitions
Now that we have finally defined identification types, we can define the structural rules for term definitions. The structural rules for term definitions say that given a term and a term definition , one could derive that is a term of , and that there is an identification between and :
Similarly, now that we have finally defined identification types, dependent function types, function types, and dependent pair types, we can define the structural rules for type definitions. The structural rules for type definitions say that given a type and a type definition , one could derive that is a type and that there is an equivalence between and :
Positive types
Now that we have identification types, dependent heterogeneous identification types, equivalence types, dependent sum types, and dependent product types, we can use that to define the equivalence type, the isContr modality, the uniqueness quantifier
and combine the elimination rule, the computation rule, and the uniqueness rule for any positive type into one rule, the universal property rule. In addition, every type has an extensionality rule.
Unit type
Formation rules for the unit type:
Introduction rules for the unit type:
Universal property rule for the unit type:
Extensionality rule for the unit type:
Empty type
Formation rules for the empty type:
Universal property rule for the empty type:
Interval type
Formation rules for the interval type:
Introduction rules for the interval type:
Universal property rule for the interval type:
Extensionality rules for the interval type:
Copy types
Formation rules for copy types:
Introduction rules for copy types:
Universal property rule for copy types:
Extensionality rules for the copy type:
Booleans type
Formation rules for the booleans type:
Introduction rules for the booleans type:
Universal property rule for the booleans type:
Extensionality rules for the booleans type:
Circle type
Formation rules for the circle type:
Introduction rules for the circle type:
Universal property rule for the circle type:
Extensionality rules for the circle type:
Sum types
Formation rules for sum types:
Introduction rules for sum types:
Universal property rule for sum types:
Extensionality rules for the sum type:
Natural numbers type
Formation rules for the natural numbers type:
Introduction rules for the natural numbers type:
Universal property rule for the natural numbers type:
Integers type
Formation rules for the integers type:
Introduction rules for the integers type:
Universal property rule for the integers type:
Localizations
The localization of a type at a type is the (higher) inductive type generated by a function and an equivalence :
Formation rules for localizations:
Introduction rules for localizations:
Disjunctions
The disjunction of a type and a type is the (higher) inductive type generated by functions and and an equivalence :
Formation rules for disjunctions:
Introduction rules for disjunctions:
Propositional truncations and set truncations
The propositional truncation of a type is localization of at the booleans type , . The set truncation of a type is localization of at the circle 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.
Open problems
There are plenty of questions which are currently unresolved in objective type theory. Van der Berg and Besten in particular listed the following problems in their article:
Other problems include
See also open problems in homotopy type theory
See also
References
-
Benno van den Berg, Martijn den Besten, Quadratic type checking for objective type theory (arXiv:2102.00905)
-
Mike Shulman, Towards a Third-Generation HOTT Part 1 (slides, video)
-
Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Project, Institute for Advanced Study, 2013. (web, pdf)
-
Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)
-
Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson, Symmetry (2021) pdf