\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 a version of homotopy type theory where all computational and uniqueness rules use the identity type rather than judgmental equality.
\subsection{Judgments and contexts}
Homotopy 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 ,
-
Judgmental equality of types, where we judge types and to be judgmentally equal,
-
Term judgments, where we judge to be an element of ,
-
Term definition judgments, where we judge to be defined as the term ,
-
Judgmental equality of terms, where we judge terms and to be judgmentally equal, .
-
Context judgments, where we judge to be a context, .
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
\subsection{Structural rules}
Within any dependent type theory, the structural rules include 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.
\subsubsection{For definitions and judgmental equality}
In addition, there are also structural rules for definition judgments and judgmental equality.
-
Formation and judgmental equality reflection rules for type definition:
-
Introduction and judgmental equality reflection rules for term definition:
-
Reflexivity of judgmental equality
-
Symmetry of judgmental equality
-
Transitivity of judgmental equality
-
Principle of substitution of judgmentally equal terms:
-
The variable conversion rule for judgmentally equal types:
\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}
Formation rule for identity types:
Introduction rule for identity types:
Elimination rule for identity types:
Computation rules for identity types:
\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:
\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
\subsection{Transport}
Transport is the statement that given a type family indexed by , elements and , and an identification , there is an equivalence 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.
\subsection{Dependent identity types}
We define the dependent identity type? as follows:
\subsection{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{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)
\section{See also}
\section{External links}