Homotopy Type Theory dependent type theory > history (Rev #5, changes)

Showing changes from revision #4 to #5: Added | ~~Removed~~ | ~~Chan~~ged

\tableofcontents

\section{Idea}

This article is about dependent type theories, which is the foundations for the rest of mathematics

time to copy half the homotopy type theory article over here.

\section{Presentation}

The model of dependent type theory we shall be presenting here is the objective type theory version of dependent 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 $A \; \mathrm{type}$ , where we judge $A$ to be a type, typing judgments, where we judge $a$ to be an element of $A$ , $a:A$ , and context judgments, where we judge $\Gamma$ to be a context, $\Gamma \; \mathrm{ctx}$ . Contexts are lists of typing judgments $a:A$ , $b:B$ , $c:C$ , et cetera, and are formalized by the rules for the empty context and extending the context by a typing judgment

\frac{}{() \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A \; \mathrm{type}}{(\Gamma, a:A) \; \mathrm{ctx}}

\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:

\frac{\vdash \Gamma, a:A, \Delta \; \mathrm{ctx}}{\vdash \Gamma, a:A, \Delta \vdash a:A}

Let $\mathcal{J}$ be any arbitrary judgment. Then we have the following rules:

The weakening rule:

\frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, \Delta \vdash \mathcal{J}}

The substitution rule:

\frac{\Gamma \vdash a:A \quad \Gamma, b:A, \Delta \vdash \mathcal{J}}{\Gamma, \Delta[a/b] \vdash \mathcal{J}[a/b]}

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.

There are other rules which could be derived from the three rules above. These include the exchange rule and the variable conversion rule.

The exchange rule:

\subsection{Dependent types and sections}

A dependent type is a type $B$ in the context of the variable judgment $x:A$ , $x:A \vdash B \; \mathrm{type}$ , they are usually written as $B(x)$ to indicate its dependence upon $x$ .

A section or dependent term is a term $b:B$ in the context of the variable judgment $x:A$ , $x:A \vdash b:B$ . Sections are likewise usually written as $b(x)$ to indicate its dependence upon $x$ .

\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:

\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash a =_A b \; \mathrm{type}}

Introduction rule for equality types:

\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A \vdash \mathrm{refl}_A(a) : a =_A a}

Elimination rule for equality types:

\frac{\Gamma, a:A, b:A, p:a =_A b \vdash C(a, b, p) \mathrm{type} \quad \Gamma, a:A \vdash t:C(a, a, \mathrm{refl}_A(a))}{\Gamma, a:A, b:A, p:a =_A b \vdash J(t, a, b, p):C(a, b, p)}

Computation rules for equality types:

\frac{\Gamma, a:A, b:A, p:a =_A b \vdash C(a, b, p) \; \mathrm{type} \quad \Gamma, a:A \vdash t:C(a, a, \mathrm{refl}_A(a))}{\Gamma, a:A, b:A, p:a =_A b \vdash \beta_{=_A}(a) : J(t, a, a, \mathrm{refl}(a)) =_{C(a, a, \mathrm{refl}_A(a))} t}

\subsection{Natural numbers}

The natural numbers are the first type introduced in mathematics, so it would be appropriate to introduce them here as well.

Formation rules for the natural numbers:

\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N} \; \mathrm{type}}

Introduction rules for the natural numbers:

\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{N}} \qquad \frac{\Gamma \vdash n:\mathbb{N}}{\Gamma \vdash s(n):\mathbb{N}}

Elimination rules for the natural numbers:

\frac{\Gamma, x:\mathbb{N} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma, x:\mathbb{N}, c:C \vdash c_s:C[s(x)/x] \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{ind}_\mathbb{N}^C(n, c_0, c_s):C[n/x]}

Computation rules for the natural numbers:

\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma, x:\mathbb{N}, c:C \vdash c_s:C[s(x)/x]}{\Gamma \vdash \beta_\mathbb{N}^{0}: \mathrm{ind}_\mathbb{N}^C(0, c_0, c_s) =_{C[0/x]} c_0}

\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma, x:\mathbb{N}, c:C \vdash c_s:C[s(x)/x]}{\Gamma \vdash \beta_\mathbb{N}^{s(n)}: \mathrm{ind}_\mathbb{N}^C(s(n), c_0, c_s) =_{C[s(n)/x]} c_s(n, \mathrm{ind}_\mathbb{N}^C(n, c_0, c_s))}

Uniqueness rules for the natural numbers:

\frac{\Gamma, x:\mathbb{N} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma, x:\mathbb{N}, c:C \vdash c_s:C[s(x)/x] \quad \Gamma \vdash n:\mathbb{N} \quad \Gamma, x:\mathbb{N} \vdash u:C \quad \Gamma \vdash i_0(u):u[0/x] =_{C[0/x]} c_0 \quad \Gamma, x:\mathbb{N} \vdash i_s(u):u[s(x)/x] =_{C[s(x)/x]} c_s[u/c]}{\Gamma \vdash \eta_\mathbb{N}(n, u):u[n/x] =_{C[n/x]} \mathrm{ind}_\mathbb{N}^{C}(p, c_0, c_s)}

\subsubsection{Addition}

Addition on the natural numbers is defined by the following rules:

Introduction rules for addition on the natural numbers:

\frac{\Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash m + n:\mathbb{N}}

Computation rules for addition on the natural numbers:

\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{basecase}_{+}:0 + 0 =_{\mathbb{N}} 0} \qquad \frac{\Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{indcaseleft}_{+}(m, n):s(m) + n =_{\mathbb{N}} s(m + n)} \qquad \frac{\Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{indcaseright}_{+}(m, n):m + s(n) =_{\mathbb{N}} s(m + n)}

\begin{theorem} Addition is associative:

\frac{\Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash p:\mathbb{N}}{\Gamma \vdash \mathrm{assoc}_{+}(m, n, p):(m + n) + p =_\mathbb{N} m + (n + p)}

\end{theorem}

\begin{proof} … \end{proof}

\subsubsection{Multiplication}

Multiplication on the natural numbers is defined by the following rules:

Introduction rules for multiplication on the natural numbers:

\frac{\Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash m \times n:\mathbb{N}}

Computation rules for multiplication on the natural numbers:

\frac{\Gamma \vdash m:\mathbb{N}}{\Gamma \vdash \mathrm{basecase}_{\times}(m):m \times 0 =_{\mathbb{N}} 0} \qquad \frac{\Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{indcase}_{\times}(m, n):m \times s(n) =_{\mathbb{N}} m \times n + m}

\section{See also}

propositional logic

type theory over logic

\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)

Revision on October 14, 2022 at 17:47:08 by Anonymous?. See the history of this page for a list of all contributions to it.