Showing changes from revision #45 to #46:
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 five the following judgments:
-
Type judgments, where we judge to be a type,
-
Type definition judgments, where we judge to be defined as the type ,
-
Term judgments, where we judge to be an element of ,
-
Term definition judgments, where we judge to be defined as the term ,
-
Context judgments, where we judge to be a context, .
-
Fresh variable judgments, where we judge to be a fresh variable,
Contexts are lists of term judgments , , , et cetera, and are formalized by the rules for the empty context and extending the context by a term judgment
Note that type and term definition judgments are not judgmental equalities; the former are single assignment operators while the latter are equivalence relations.
\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 term judgment if the term 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{Sections and dependent types}
A dependent type is a type in the context of the variable judgment , . A section is a term in the context of the variable judgment , .
\subsection{Identity types}
Equality in objective type theory is represented by the identity type, which is also called the path type or identification type. The terms of the identity type could be called paths or identifications.
Equality comes with a formation rule, an introduction rule, an elimination rule, and a computation rule:
Formation rule for identity types:
Introduction rule for identity types:
Elimination rule for identity types:
Computation rules for identity types:
The uniqueness rule for identity types? is usually not included in objective type theory. However, if it were included in objective type theory it turns the type theory into a set-level type theory?.
\subsection{Structural rules for definitions}
Now that we have finally defined identity types, we can define the structural rules for definitions. The structural rules for term definitions say that given a term definition judgment , one could derive that is a term of , and that there is an identification between and :
The structural rules for type definitions are the natural deduction rules for copying types, with formation and introduction rules:
elimination rules:
computation rules:
and uniqueness rules:
\subsection{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:
Ordinary function types are a special type of dependent function types, as the weakening rule implies that one could derive
and thus the dependent function type
which is not dependent on . Thus, we could define the ordinary function type as
\subsection{Dependent pair types}
Ordinary product types are a special type of dependent pair types.
\subsection{Equivalence types}
Given a type , we define the type representing whether is a contractible type as
Given types and , function , and element , we define the fiber of at as
Given types and and function , we define the type representing whether is a equivalence of types? as
Given types and , we define the type of equivalences as
The equivalence types between two types and behaves as the equality between and , in the same way that the identity type between two terms and behaves as the equality between and . This is similar to structural set theory? whose type of sets have no primitive equality relation, where bijection? behaves as the equality between sets and .
\subsection{Structural rules for equality and equivalence}
\subsubsection{Variable conversion}
\subsubsection{Reflexivity}
\subsubsection{Identity equivalence}
\subsubsection{Symmetry}
\subsubsection{Inverse equivalence}
\subsubsection{Transitivity}
\subsubsection{Composition of equivalences}
\subsubsection{Transport}
Transport is the statement that given a type family indexed by and elements and , there is a function from the identity type of and to the type of equivalences between the types and . This is inductively defined on reflexivity on , which transport takes to the identity function on , .
Transport is given by the following rules:
Transport is very important in defining higher inductive types in objective type theory.
\subsubsection{Dependent identity types}
We define the dependent identity type? as follows:
\subsubsection{Dependent actions on identifications}
Additionally, for a term in the context of , there is a dependent identification? called the dependent action on identifications? for all , , and , inductively defined by reflexivity for all .
The rules for are as follows
\section{Old presentation}
\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{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{Sum types}
Formation rules for sum types:
Introduction rules for sum types:
Elimination rules for sum types:
Computation rules for sum types:
Uniqueness rules for sum types:
\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:
\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)
-
Marc Bezem?, Ulrik Buchholtz, Pierre Cagne?, Bjørn Ian Dundas?, Daniel R. Grayson, Symmetry? (2021) pdf
-
Benno van den Berg, Martijn den Besten, Quadratic type checking for objective type theory (arXiv:2102.00905)
\section{See also}
\section{External links}