Showing changes from revision #26 to #27:
Added | Removed | Changed
\tableofcontents
\section{Idea}
Homotopy type theory is a framework of dependent type theories which additionally consists of
\section{Presentation}
The model of homotopy type theory we shall be presenting here is the objective type theory version of homotopy type theory. There are multiple reasons for this:
-
Since objective type theory lacks definitional equality,
-
The ruleset is simpler in the objective type theory model of homotopy type theory than other models such as Martin-Löf type theory, cubical type theory, or higher observational type theory
-
The results in objective type theory are more general than in models which use definitional equality
-
It 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, which is propositional equality in both objective type theory and set theory, and uses propositional equality to define terms and types.
-
From a more practical standpoint, objective type theory not only has decidable type checking, it has polynomial (quadratic) time type checking, which makes it efficient from a computational standpoint.
\subsection{Judgments and contexts}
Objective type theory consists of three judgments: type judgments , where we judge to be a type, typing judgments, where we judge to be an element of , , and context judgments, where we judge to be a context, . Contexts are lists of typing judgments , , , et cetera, and are formalized by the rules for the empty context and extending the context by a typing judgment
\subsection{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 typing judgment if the typing 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.
\subsection{Dependent types and sections}
A dependent type is a type in the context of the variable judgment , , they are usually written as to indicate its dependence upon .
A section or dependent term is a term in the context of the variable judgment , . Sections are likewise usually written as to indicate its dependence upon .
\subsection{Equality}
Equality of elements of a type in objective type theory is represented by a type known as the equality type or the type of equalities. The elements of the equality type are called equalities.
Equality comes with a formation rule, an introduction rule, an elimination rule, and a computation rule:
Formation rule for equality types:
Introduction rule for equality types:
Elimination rule for equality types:
Computation rules for equality types:
\subsection{Centers of contraction}
Given a type , a term is a center of contraction? if for all there is an element . This motivates the definition of types, whose elements are proofs that is a center of contraction.
Formation rules for isCentrContr types:
Introduction rules for isCentrContr types:
Elimination rules for isCentrContr types:
Computation rules for isCentrContr types:
Uniqueness rules for isCentrContr types:
A term of a type is a center of contraction if it has an element .
\subsection{Contractible types}
A type is true, a singleton, or contractible if has a term and a term . This motivates the definition of types, whose elements are proofs that is contractible.
Formation rules for isContr types:
Introduction rules for isContr types:
Elimination rules for isContr types:
Computation rules for isContr types:
Uniqueness rules for isContr types:
A type is contractible if it has an element .
\subsection{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:
\subsection{Fibers}
In set theory, the fiber of a function with domain? and codomain? at an element in is the indexed disjoint union? of all elements such that . This definition could also be translated into objective type theory: the fiber of a function at the element is the type
This motivates the definition of fiber types, whose elements are the fibers of the function at element
Formation rules for fiber types:
Introduction rules for fiber types:
Elimination rules for fiber types:
Computation rules for fiber types:
Uniqueness rules for fiber types:
\subsection{Pi types}
Formation rules for Pi types:
Introduction rules for Pi types:
Elimination rules for Pi types:
Computation rules for Pi types:
Uniqueness rules for Pi types:
\subsection{Product types}
We use the negative presentation for product types.
Formation rules for product types:
Introduction rules for product types:
Elimination rules for product types:
Computation rules for product types:
Uniqueness rules for product types:
\subsection{Sigma types}
We use the negative presentation for sigma types.
Formation rules for Sigma types:
Introduction rules for Sigma types:
Elimination rules for Sigma types:
Computation rules for Sigma types:
Uniqueness rules for Sigma types:
\subsection{Fibers}
In set theory, the fiber of a function with domain? and codomain? at an element in is the indexed disjoint union? of all elements such that . This definition could also be translated into objective type theory: the fiber of a function at the element is the type
This motivates the definition of fiber types, whose elements are the fibers of the function at element
Formation rules for fiber types:
Introduction rules for fiber types:
Elimination rules for fiber types:
Computation rules for fiber types:
Uniqueness rules for fiber types:
Equivalences
In set theory, a function is a bijection? if all its fibers at every element of the codomain are singletons. This definition can be translated over to objective type theory, but the name used for such a function in objective type theory is equivalence? : . A function is an equivalence if there is an element
This motivates the definition of the isEquiv type family, whose elements witnesses that the function is an equivalence.
Formation rules for isEquiv types:
Introduction rules for isEquiv types:
Elimination rules for isEquiv types:
Computation rules for isEquiv types:
Uniqueness rules for isEquiv types:
The type of equivalences is given by
Definitions
Parts of the following section is adapted from Egbert Rijke’s Introduction to Homotopy Type Theory?:
We can make definitions at the end of a derivation if the conclusion is a certain type in context, or if the conclusion is a certain term of a type in context. In the case where the conclusion is a certain term of a type in context, where we have a derivation
if we wish to make a definition , then we can extend the derivation tree with
The effect of such a definition is that we have extended our type theory with a new constant , for which the following inference rules are valid
In the case where the conclusion is a certain type in context, where we have a derivation
if we wish to make a definition , then we can similarly extend the derivation tree with
The effect of such a definition in this case is that we have extended our type theory with a new constant , for which the following inference rules are valid
In essence, we define an element to be equal to , and a type to be equivalent to , in the same way that in structural set theory?, which usually also doesn’t have definitional equality, one would define element to be equal to and set to be in bijection? with .
This allows us to define and use constants for certain long and unwieldy types, such as the type of equivalences defined in the previous section:
\subsection{Empty type}
Formation rules for the empty type:
Elimination rules for the empty type:
Uniqueness rules for the empty type:
\subsection{Unit type}
Formation rules for the unit type:
Introduction rules for the unit type:
Elimination rules for the unit type:
Computation rules for the unit type:
Uniqueness rules for the unit type:
\subsection{Booleans}
Formation rules for the booleans:
Introduction rules for the booleans:
Elimination rules for the booleans:
Computation rules for the booleans:
Uniqueness rules for the booleans:
\subsection{Natural numbers}
Formation rules for the natural numbers:
Introduction rules for the natural numbers:
Elimination rules for the natural numbers:
Computation rules for the natural numbers:
Uniqueness rules for the natural numbers:
\subsection{Function extensionality}
\subsection{Universes}
Universe formation
Hierarchy formation
Type reflection
Lifting
Univalence
\section{References}
-
Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study, 2013. (web, pdf)
-
Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (pdf) (478 pages)
-
Benno van den Berg, Martijn den Besten, Quadratic type checking for objective type theory (arXiv:2102.00905)
\section{See also}
\section{External links}