Homotopy Type Theory homotopy type theory > history (Rev #32, changes)

Showing changes from revision #31 to #32: Added | Removed | Changed

\tableofcontents

\section{Idea}

Homotopy type theory is a framework of dependent type theories which additionally consists of

• identity types

• dependent product types

• dependent sum types

• univalence

• inductive types, higher inductive types, inductive type families, et cetera.

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

\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 $\mathcal{J}$ 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 $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} \subsection{Identity types}

Equality of elements of a type in objective type theory is represented by a type known as theequality typeidentity type , which is also called the path type or identification type. The terms of the identity type could be called paths or identifications.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 identity types:

Introduction rule for equality identity types:

Elimination rule for equality identity types:

Computation rules for equality identity types:

\subsection{isProp The types}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?.

In \subsection{Definitions set of theory, elements} a set is asubsingleton? if it has at most one element up to equality: every two elements in the set are equal to each other.

These Parts same of definitions the carry following over section to is objective adapted type from theory: a type$T$Egbert Rijke ’s is a subsingleton or an h-proposition Introduction to Homotopy Type Theory? : if for all$x:T$ and $y:T$ there is an element $p(x, y):x =_T y$.

This We motivates can make definitions at the definition end of a derivation if the conclusion is a certain term of a type in context, where we have a derivation$\mathrm{isProp}$ types, whose elements $p:\mathrm{isProp}(T)$ are proofs that $T$ is a proposition.

Formation rules for isProp types:

$$\frac{\mathcal{D}}{\Gamma \vdash a:A}$$

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A \vdash x =_A y \; \mathrm{type}}{\Gamma \vdash \mathrm{isProp}(A) \; \mathrm{type}}$$

if we wish to make a definition $b \coloneqq a$, then we can extend the derivation tree with

Introduction rules for isProp types:

$$\frac{\Gamma \vdash a:A}{\Gamma \vdash b \coloneqq a:A}$$

$$\frac{\Gamma, x:A, y:A \vdash p(x, y):x =_A y}{\Gamma \vdash \lambda(x).\lambda(y).p(x, y):\mathrm{isProp}(A)}$$

The effect of such a definition is that we have extended our type theory with a new constant $b$, for which the following inference rules are valid

Elimination rules for isProp types:

$$\frac{\mathcal{D}}{b:A} \qquad \frac{\mathcal{D}}{\mathrm{defeq}(a, b):b =_A a}$$

$$\frac{\Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A}{\Gamma \vdash p(a, b):a =_A b}$$

Computation rules for isProp types:

$$\frac{\Gamma, x:A, y:A \vdash p(x, y):x =_A y \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A}{\Gamma \vdash \beta_\mathrm{isProp}:(\lambda(x).\lambda(y).p(x, y))(a, b) =_{a =_A b} p(a, b)}$$

Uniqueness rules for isProp types:

$$\frac{\Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \eta_\mathrm{isProp}:p =_{\mathrm{isProp}(A)} \lambda(x).\lambda(y).p(x, y)}$$

\subsection{isContr types}

In set theory, a set is a pointed set? if it has at least one chosen element, and it is a singleton? if it has exactly one element up to equality: it is a pointed set and a subsingleton.

These same definitions carry over to objective type theory: A type $T$ is a pointed type if it has a chosen element $a:T$, a type $T$ is a singleton if it has both an element $p_*:T$ and an element $q:\mathrm{isProp}(T)$, or equivalently, an element

$$c:T \times \mathrm{isProp}(T)$$

This motivates the definition of $\mathrm{isContr}$ types, whose elements $p:\mathrm{isContr}(T)$ are proofs that $T$ is contractible.

Formation rules for isContr types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash \mathrm{isProp}(A) \; \mathrm{type}}{\Gamma \vdash \mathrm{isContr}(A) \; \mathrm{type}}$$

Introduction rules for isContr types:

$$\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:\mathrm{isProp}(A)}{\Gamma \vdash (a, b):\mathrm{isContr}(A)}$$

Elimination rules for isContr types:

$$\frac{\Gamma \vdash z:\mathrm{isContr}(A)}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:\mathrm{isContr}(A)}{\Gamma \vdash \pi_2(z):\mathrm{isProp}(A)}$$

Computation rules for isContr types:

$$\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:\mathrm{isProp}(A)}{\Gamma \vdash \beta_{\mathrm{isContr} 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:\mathrm{isProp}(A)}{\Gamma \vdash \beta_{\mathrm{isContr} 2}:\pi_2(a, b) =_{\mathrm{isProp}(A)} b}$$

Uniqueness rules for isContr types:

$$\frac{\Gamma \vdash z:\mathrm{isContr}(A)}{\Gamma \vdash \eta_{\mathrm{isContr}}:z =_{\mathrm{isContr}(A)} (\pi_1(z), \pi_2(z))}$$

\subsection{Function types}

Formation rules for function types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \to B \; \mathrm{type}}$$

Introduction rules for function types:

$$\frac{\Gamma, x:A \vdash b(x):B}{\Gamma \vdash (x \mapsto b(x)):A \to B}$$

Elimination rules for function types:

$$\frac{\Gamma \vdash f:A \to B \quad \Gamma \vdash a:A}{\Gamma \vdash f(a):B}$$

Computation rules for function types:

$$\frac{\Gamma, x:A \vdash b(x):B \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\to}:(x \mapsto b(x))(a) =_{B} b}$$

Uniqueness rules for function types:

$$\frac{\Gamma \vdash f:A \to B}{\Gamma \vdash \eta_{\to}:f =_{A \to B} (x \to f(x))}$$

\subsection{Fibers}

In set theory, the fiber of a function $f$ with domain? $A$ and codomain? $B$ at an element $b$ in $B$ is the indexed disjoint union? of all elements $a:A$ such that $f(a) = b$. This definition could also be translated into objective type theory: the fiber of a function $f:A \to B$ at the element $b:B$ is the type

$$\sum_{a:A} f(a) =_B b$$

This motivates the definition of fiber types, whose elements $p:\mathrm{fiber}_{A, B}(f, y)$ are the fibers of the function $f:A \to B$ at element $y:B$

Formation rules for fiber types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B, y:B, x:A \vdash f(x) =_B y \; \mathrm{type}}{\Gamma, f:A \to B, y:B \vdash \mathrm{fiber}_{A, B}(f, y) \; \mathrm{type}}$$

Introduction rules for fiber types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B, y:B, x:A \vdash b(x):f(x) =_B y \quad \Gamma \vdash a:A \quad \Gamma, f:A \to B, y:B \vdash p:f[a/x] =_B y}{\Gamma, f:A \to B, y:B \vdash (a, b):\mathrm{fiber}_{A, B}(f, y)}$$

Elimination rules for fiber types:

$$\frac{\Gamma, f:A \to B, y:B \vdash z:\mathrm{fiber}_{A, B}(f, y)}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma, f:A \to B, y:B \vdash z:\mathrm{fiber}_{A, B}(f, y)}{\Gamma, f:A \to B, y:B \vdash \pi_2(z):f(\pi_1(z)) =_B y}$$

Computation rules for fiber types:

$$\frac{\Gamma, f:A \to B, y:B, x:A \vdash b(x):f(x) =_B b \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\mathrm{fiber}_{A, B} 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma, f:A \to B, y:B, x:A \vdash b(x):f(x) =_B y \quad \Gamma \vdash a:A}{\Gamma, f:A \to B, y:B \vdash \beta_{\mathrm{fiber}_{A, B} 2}:\pi_2(a, b) =_{f(\pi_1(a, b)) =_B y} b}$$

Uniqueness rules for fiber types:

$$\frac{\Gamma, f:A \to B, y:B \vdash z:\mathrm{fiber}_{A, B}(f, y)}{\Gamma, f:A \to B, y:B \vdash \eta_{\mathrm{fiber}_{A, B}}:z =_{\mathrm{fiber}_{A, B}(f, y)} (\pi_1(z), \pi_2(z))}$$

\subsection{isEquiv types}

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?.

This motivates the definition of the isEquiv type family, whose elements $p:\mathrm{isEquiv}_{A, B}(f)$ witnesses that the function $f:A \to B$ is an equivalence.

Formation rules for isEquiv types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B, y:B \vdash \mathrm{isContr}(\mathrm{fiber}_{A, B}(f, y)) \; \mathrm{type}}{\Gamma \vdash \mathrm{isEquiv}_{A, B}(f) \; \mathrm{type}}$$

Introduction rules for isEquiv types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B, y:B \vdash b(y):\mathrm{isContr}(\mathrm{fiber}_{A, B}(f, y))}{\Gamma, f:A \to B \vdash \lambda x.b(x):\mathrm{isEquiv}_{A, B}(f)}$$

Elimination rules for isEquiv types:

$$\frac{\Gamma, f:A \to B \vdash p:\mathrm{isEquiv}_{A, B}(f) \quad \Gamma \vdash c:B}{\Gamma, f:A \to B \vdash p(a):\mathrm{isEquiv}_{A, B}(f)(c)}$$

Computation rules for isEquiv types:

$$\frac{\Gamma, f:A \to B, y:B \vdash b(y):\mathrm{isContr}(\mathrm{fiber}_{A, B}(f, y)) \quad \Gamma \vdash c:B}{\Gamma, f:A \to B \vdash \beta_\mathrm{isEquiv}:\lambda x.b(x)(c) =_{\mathrm{isContr}(\mathrm{fiber}_{A, B}(f, c))} b(c)}$$

Uniqueness rules for isEquiv types:

$$\frac{\Gamma, f:A \to B \vdash p:\mathrm{isEquiv}_{A, B}(f)}{\Gamma, f:A \to B \vdash \eta_\mathrm{isEquiv}:p =_{\mathrm{isEquiv}_{A, B}(f)} \lambda(x).p(x)}$$

\subsection{Equivalence types}

The type of equivalences is given by the following rules

Formation rules for equivalence types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B \vdash \mathrm{isEquiv}(f) \; \mathrm{type}}{\Gamma \vdash A \simeq B \; \mathrm{type}}$$

Introduction rules for equivalence types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B \vdash p(f):\mathrm{isEquiv}(f) \quad \Gamma \vdash g:A \to B \quad \Gamma \vdash p:\mathrm{isEquiv}[g/f]}{\Gamma \vdash (g, p):A \simeq B}$$

Elimination rules for equivalence types:

$$\frac{\Gamma \vdash h:A \simeq B}{\Gamma \vdash \pi_1(h):A \to B} \qquad \frac{\Gamma \vdash h:A \simeq B}{\Gamma \vdash \pi_2(h):\mathrm{isEquiv}(\pi_1(z))}$$

Computation rules for equivalence types:

$$\frac{\Gamma, f:A \to B \vdash p(f):\mathrm{isEquiv}(f) \quad \Gamma \vdash g:A \to B}{\Gamma \vdash \beta_{\simeq 1}:\pi_1(g, p) =_{A \to B} g} \qquad \frac{\Gamma, f:A \to B \vdash p:\mathrm{isEquiv} \quad \Gamma \vdash g:A \to B}{\Gamma \vdash \beta_{\simeq 2}:\pi_2(g, p) =_{\mathrm{isEquiv}(\pi_1(g, p))} p}$$

Uniqueness rules for equivalence types:

$$\frac{\Gamma \vdash h:A \simeq B}{\Gamma \vdash \eta_\simeq:h =_{A \simeq B} (\pi_1(h), \pi_2(h))}$$

\subsection{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

$$\frac{\mathcal{D}}{\Gamma \vdash a:A}$$

if we wish to make a definition $b \coloneqq a$, then we can extend the derivation tree with

$$\frac{\Gamma \vdash a:A}{\Gamma \vdash b \coloneqq a:A}$$

The effect of such a definition is that we have extended our type theory with a new constant $b$, for which the following inference rules are valid

$$\frac{\mathcal{D}}{b:A} \qquad \frac{\mathcal{D}}{\mathrm{defeq}(a, b):b =_A a}$$

In the case where the conclusion is a certain type in context, where we have a derivation

$$\frac{\mathcal{D}}{\Gamma \vdash A \; \mathrm{type}}$$

if we wish to make a definition $B \coloneqq A$, then we can similarly extend the derivation tree with

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash B \coloneqq A \; \mathrm{type}}$$

The effect of such a definition in this case is that we have extended our type theory with a new constant $B$, for which the following inference rules are valid

$$\frac{\mathcal{D}}{B \; \mathrm{type}} \qquad \frac{\mathcal{D}}{\mathrm{defequiv}(B, A): B \simeq A}$$

In essence, we define an element $b$ to be equal to $a$, and a type $B$ to be equivalent to $A$, in the same way that in structural set theory?, which usually also doesn’t have definitional equality, one would define element $b$ to be equal to $a$ and set $B$ to be in bijection? with $A$.

\subsection{H-levels}

Suppose the dependent type theory has identity types, contraction types?, and a natural numbers type?. Then one could define the type family $\mathrm{hasHLevel}(n, A)$ for all types $A$ in the context of the natural numbers variable $n:\mathrm{N}$ with the following rules:

Formation rules for hasHLevel types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash \mathrm{Contr}_A(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{hasHLevel}(0, A) \; \mathrm{type}}$$

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, n:\mathbb{N}, x:A, y:A \vdash \mathrm{hasHLevel}(n, x =_A y) \; \mathrm{type}}{\Gamma \vdash \mathrm{hasHLevel}(s(n), A) \; \mathrm{type}}$$

Introduction rules for hasHLevel types:

$$\frac{\Gamma, x:A \vdash b(x):\mathrm{Contr}_A(x) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:\mathrm{Contr}_A[a/x]}{\Gamma \vdash (a, b):\mathrm{hasHLevel}(0, A)}$$

$$\frac{\Gamma, n:\mathbb{N}, x:A, y:A \vdash p(n, x, y):\mathrm{hasHLevel}(n, x =_A y)}{\Gamma, n:\mathbb{N} \vdash \lambda(x).\lambda(y).p(n, x, y):\mathrm{hasHLevel}(s(n), A)}$$

Elimination rules for hasHLevel types:

$$\frac{\Gamma \vdash z:\mathrm{hasHLevel}(0, A)}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:\mathrm{hasHLevel}(0, A)}{\Gamma \vdash \pi_2(z):\mathrm{Contr}_A(\pi_1(z))}$$

$$\frac{\Gamma, n:\mathbb{N} \vdash p:\mathrm{hasHLevel}(s(n), A) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A}{\Gamma, n:\mathbb{N} \vdash p(n, a, b):\mathrm{hasHLevel}(n, x =_A y)}$$

Computation rules for hasHLevel types:

$$\frac{\Gamma, x:A \vdash b(x):\mathrm{Contr}_A(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\mathrm{hasHLevel}^0 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma, x:A \vdash b(x):\mathrm{Contr}_A(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\mathrm{hasHLevel}^0 2}:\pi_2(a, b) =_{\mathrm{Contr}_A(a)} b}$$

$$\frac{\Gamma, n:\mathrm{N}, x:A, y:A \vdash p(n, x, y):\mathrm{hasHLevel}(n, x =_A y) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A}{\Gamma, n:\mathrm{N} \vdash \beta_{\mathrm{hasHLevel}^s}:(\lambda(x).\lambda(y).p(n, x, y))(a, b) =_{\mathrm{hasHLevel}(n, x =_A y)} p(n, a, b)}$$

Uniqueness rules for hasHLevel types:

$$\frac{\Gamma \vdash z:\mathrm{hasHLevel}(0, A)}{\Gamma \vdash \eta_{\mathrm{hasHLevel}^0}:z =_{\mathrm{hasHLevel}(0, A)} (\pi_1(z), \pi_2(z))}$$

$$\frac{\Gamma, n:\mathbb{N} \vdash p:\mathrm{hasHLevel}(s(n), A)}{\Gamma, n:\mathbb{N} \vdash \eta_{\mathrm{hasHLevel}^s}:p(n) =_{\mathrm{hasHLevel}(s(n), A)} \lambda(x).\lambda(y).p(n, x, y)}$$

\subsection{Pi types}

Formation rules for Pi types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \prod_{x:A} B(x) \; \mathrm{type}}$$

Introduction rules for Pi types:

$$\frac{\Gamma, x:A \vdash b(x):B(x)}{\Gamma \vdash \lambda(x:A).b(x):\prod_{x:A} B(x)}$$

Elimination rules for Pi types:

$$\frac{\Gamma \vdash f:\prod{x:A} B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash f(a):B[a/x]}$$

Computation rules for Pi types:

$$\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_\Pi:\lambda(x:A).b(x)(a) =_{B[a/x]} b[a/x]}$$

Uniqueness rules for Pi types:

$$\frac{\Gamma \vdash f:\prod_{x:A} B(x)}{\Gamma \vdash \eta_\Pi:f =_{\prod_{x:A} B(x)} \lambda(x).f(x)}$$

\subsection{Product types}

We use the negative presentation for product types.

Formation rules for product types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \times B \; \mathrm{type}}$$

Introduction rules for product types:

$$\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash (a, b):A \times B}$$

Elimination rules for product types:

$$\frac{\Gamma \vdash z:A \times B}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:A \times B}{\Gamma \vdash \pi_2(z):B}$$

Computation rules for product types:

$$\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash \beta_{\times 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash \beta_{\times 2}:\pi_2(a, b) =_B b}$$

Uniqueness rules for product types:

$$\frac{\Gamma \vdash z:A \times B}{\Gamma \vdash \eta_\times:z =_{A \times B} (\pi_1(z), \pi_2(z))}$$

\subsection{Sigma types}

We use the negative presentation for sigma types.

Formation rules for Sigma types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \sum_{x:A} B(x) \; \mathrm{type}}$$

Introduction rules for Sigma types:

$$\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B[a/x]}{\Gamma \vdash (a, b):\sum_{x:A} B(x)}$$

Elimination rules for Sigma types:

$$\frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash \pi_2(z):B(\pi_1(z))}$$

Computation rules for Sigma types:

$$\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\Sigma 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma, x:A \vdash b:B \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\Sigma 2}:\pi_2(a, b) =_{B\pi_1(a, b)} b}$$

Uniqueness rules for Sigma types:

$$\frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash \eta_\Sigma:z =_{\sum_{x:A} B(x)} (\pi_1(z), \pi_2(z))}$$

\subsection{Sum types}

Formation rules for sum types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A + B \; \mathrm{type}}$$

Introduction rules for sum types:

$$\frac{\Gamma \vdash a:A}{\Gamma \vdash \mathrm{inl}(a):A + B} \qquad \frac{\Gamma \vdash b:B}{\Gamma \vdash \mathrm{inr}(b):A + B}$$

Elimination rules for sum types:

$$\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{inl}(x)) \quad \Gamma, y:B \vdash d(y):C(\mathrm{inr}(y)) \quad \Gamma \vdash e:A + B}{\Gamma \vdash \mathrm{ind}_{A + B}^C(c(x), d(y), e):C(e)}$$

Computation rules for sum types:

$$\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{inl}(x)) \quad \Gamma, y:B \vdash d(y):C(\mathrm{inr}(y)) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_1:\mathrm{ind}_{A + B}^C(c(x), d(y), \mathrm{inl}(a)) =_{C(\mathrm{inl}(a))} c(a)}$$

$$\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{inl}(x)) \quad \Gamma, y:B \vdash d(y):C(\mathrm{inr}(y)) \quad \Gamma \vdash b:B}{\Gamma \vdash \beta_2:\mathrm{ind}_{A + B}^C(c(x), d(y), \mathrm{inr}(b)) =_{C(\mathrm{inr}(b))} d(b)}$$

Uniqueness rules for sum types:

$$\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{inl}(x)) \quad \Gamma, y:B \vdash d(y):C(\mathrm{inr}(y)) \quad \Gamma \vdash e:A + B \quad \Gamma, x:A + B \vdash u:C \quad \Gamma, a:A \vdash i_\mathrm{inl}(u):u(\mathrm{inl}(a)) =_{C(\mathrm{inl}(a))} c(a) \quad \Gamma, b:B \vdash i_\mathrm{inr}(u):u(\mathrm{inr}(b)) =_{C(\mathrm{inr}(b))} d(b)}{\Gamma \vdash \eta_{A + B}:u(e) =_{C(e)} \mathrm{ind}_{A + B}^C(c(\mathrm{inl}(e)), d(\mathrm{inl}(e)), e)}$$

\subsection{Empty type}

Formation rules for the empty type:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{0} \; \mathrm{type}}$$

Elimination rules for the empty type:

$$\frac{\Gamma, x:\mathbb{0} \vdash C \; \mathrm{type} \quad \Gamma \vdash p:\mathbb{0}}{\Gamma \vdash \mathrm{ind}_\mathbb{0}^C(p):C(p)}$$

Uniqueness rules for the empty type:

$$\frac{\Gamma, x:\mathbb{0} \vdash C \; \mathrm{type} \quad \Gamma \vdash p:\mathbb{0} \quad \Gamma, x:\mathbb{0} \vdash u:C}{\Gamma \vdash \eta_\mathbb{0}(p, u):u[p/x] =_{C[p/x]} \mathrm{ind}_\mathbb{0}^{C}(p)}$$

\subsection{Unit type}

Formation rules for the unit type:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{1} \; \mathrm{type}}$$

Introduction rules for the unit type:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash *:\mathbb{1}}$$

Elimination rules for the unit type:

$$\frac{\Gamma, x:\mathbb{1} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_*:C[*/x] \quad \Gamma \vdash p:\mathbb{1}}{\Gamma \vdash \mathrm{ind}_\mathbb{1}^C(p, c_*):C[p/x]}$$

Computation rules for the unit type:

$$\frac{\Gamma, x:\mathbb{1} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_*:C[*/x]}{\Gamma \vdash \beta_\mathbb{1}: \mathrm{ind}_\mathbb{1}^C(*, c_*) =_{C[*/x]} c_*}$$

Uniqueness rules for the unit type:

$$\frac{\Gamma, x:\mathbb{1} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_*:C[*/x] \quad \Gamma \vdash p:\mathbb{1} \quad \Gamma, x:\mathbb{1} \vdash u:C \quad \Gamma \vdash i_*(u):u[*/x] =_{C[*/x]} c_* }{\Gamma \vdash \eta_\mathbb{1}(p, u):u[p/x] =_{C[p/x]} \mathrm{ind}_\mathbb{1}^{C}(p, c_*)}$$

\subsection{Booleans}

Formation rules for the booleans:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{2} \; \mathrm{type}}$$

Introduction rules for the booleans:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{2}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathbb{2}}$$

Elimination rules for the booleans:

$$\frac{\Gamma, x:\mathbb{2} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma \vdash c_1:C[1/x] \quad \Gamma \vdash p:\mathbb{2}}{\Gamma \vdash \mathrm{ind}_\mathbb{2}^{C}(p, c_0, c_1):C[p/x]}$$

Computation rules for the booleans:

$$\frac{\Gamma, x:\mathbb{2} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma \vdash c_1:C[1/x]}{\Gamma \vdash \beta_\mathbb{2}^{0}: \mathrm{ind}_\mathbb{2}^{C}(0, c_0, c_1) =_{C[0/x]} c_0}$$

$$\frac{\Gamma, x:\mathbb{2} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma \vdash c_1:C[1/x]}{\Gamma \vdash \beta_\mathbb{2}^{1}: \mathrm{ind}_\mathbb{2}^{C}(1, c_0, c_1) =_{C[1/x]} c_1}$$

Uniqueness rules for the booleans:

$$\frac{\Gamma, x:\mathbb{2} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma \vdash c_1:C[1/x] \quad \Gamma \vdash p:\mathbb{2} \quad \Gamma, x:\mathbb{2} \vdash u:C \quad \Gamma \vdash i_0(u):u[0/x] =_{C[0/x]} c_0 \quad \Gamma \vdash i_1(u):u[1/x] =_{C[1/x]} c_1}{\Gamma \vdash \eta_\mathbb{2}(p, u):u[p/x] =_{C[p/x]} \mathrm{ind}_\mathbb{2}^{C}(p, c_0, c_1)}$$

\subsection{Natural numbers}

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)}$$

\subsection{Function \subsection{isProp extensionality} types}

In set theory, a set is a subsingleton? if it has at most one element up to equality: every pair of elements in the set are equal to each other.

These same definitions carry over to objective type theory: a type $T$ is a subsingleton or an h-proposition? if for all pairs $x:T \times T$ there is an element $\mathrm{proptrunc}(x):\pi_1(x) =_T \pi_2(x)$. Since objective type theory has Pi types, this is the same as saying that there is a dependent function

$$\mathrm{proptrunc}:\prod_{x:T \times T} \pi_1(x) =_T \pi_2(x)$$

The elements $p:\prod_{x:T \times T} \pi_1(x) =_T \pi_2(x)$ are proofs that $T$ is a proposition or subsingleton.

We could use the type $\prod_{x:T \times T} \pi_1(x) =_T \pi_2(x)$ wherever we want to see if a type is a subsingleton or proposition, but it is somewhat cumbersome to write out, and we would like to abbreviate that to the type $\mathrm{isProp}(T)$. This motivates introducing rules for $\mathrm{isProp}$ types separate from the existing rules for Pi types. (Later, after we have defined equivalences $A \simeq B$, we could just introduce the type $\mathrm{isProp}(T)$ and an equivalence $\mathrm{isProp}(T) \simeq \prod_{x:T \times T} \pi_1(x) =_T \pi_2(x)$.)

Formation rules for isProp types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \times A \vdash \pi_1(x) =_A \pi_2(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{isProp}(A) \; \mathrm{type}}$$

Introduction rules for isProp types:

$$\frac{\Gamma, x:A \times A \vdash p(x):\pi_1(x) =_A \pi_2(x)}{\Gamma \vdash \lambda x.p(x):\mathrm{isProp}(A)}$$

Elimination rules for isProp types:

$$\frac{\Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash a:A \times A}{\Gamma \vdash p(a):\pi_1(a) =_A \pi_2(a)}$$

Computation rules for isProp types:

$$\frac{\Gamma, x:A \times A \vdash p(x):\pi_1(x) =_A \pi_2(x) \quad \Gamma \vdash a:A \times A}{\Gamma \vdash \beta_\mathrm{isProp}:(\lambda x.p(x))(a) =_{\pi_1(a) =_A \pi_2(a)} p(a)}$$

Uniqueness rules for isProp types:

$$\frac{\Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \eta_\mathrm{isProp}:p =_{\mathrm{isProp}(A)} \lambda x.p(x)}$$

\subsection{isContr types}

In set theory, a set is a pointed set? if it has at least one chosen element, and it is a singleton? if it has exactly one element up to equality: it is a pointed set and a subsingleton.

These same definitions carry over to objective type theory: A type $T$ is a pointed type if it has a chosen element $a:T$, a type $T$ is a singleton or a contractible type if it has both an element $p_*:T$ and an element $q:\mathrm{isProp}(T)$, or equivalently, an element

$$p:T \times \mathrm{isProp}(T)$$

The elements $p:\T \times \mathrm{isProp}(T)$ are proofs that $T$ is a singleton or a contractible type.

Similarly to the case for isProp types, we could use the type $T \times \mathrm{isProp}(T)$ wherever we want to see if a type is a singleton or contractible, but it is similarly cumbersome to write out, and we would like to abbreviate that to the type $\mathrm{isContr}(T)$. This motivates introducing rules for $\mathrm{isContr}$ types separate from the existing rules for product types:

Formation rules for isContr types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash \mathrm{isProp}(A) \; \mathrm{type}}{\Gamma \vdash \mathrm{isContr}(A) \; \mathrm{type}}$$

Introduction rules for isContr types:

$$\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:\mathrm{isProp}(A)}{\Gamma \vdash (a, b):\mathrm{isContr}(A)}$$

Elimination rules for isContr types:

$$\frac{\Gamma \vdash z:\mathrm{isContr}(A)}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:\mathrm{isContr}(A)}{\Gamma \vdash \pi_2(z):\mathrm{isProp}(A)}$$

Computation rules for isContr types:

$$\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:\mathrm{isProp}(A)}{\Gamma \vdash \beta_{\mathrm{isContr} 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:\mathrm{isProp}(A)}{\Gamma \vdash \beta_{\mathrm{isContr} 2}:\pi_2(a, b) =_{\mathrm{isProp}(A)} b}$$

Uniqueness rules for isContr types:

$$\frac{\Gamma \vdash z:\mathrm{isContr}(A)}{\Gamma \vdash \eta_{\mathrm{isContr}}:z =_{\mathrm{isContr}(A)} (\pi_1(z), \pi_2(z))}$$

\subsection{Fiber types}

In set theory, the fiber of a function $f$ with domain? $A$ and codomain? $B$ at an element $b$ in $B$ is the indexed disjoint union? of all elements $a:A$ such that $f(a) = b$. This definition could also be translated into objective type theory: the fiber of a function $f:A \to B$ at the element $b:B$ is the type

$$\sum_{a:A} f(a) =_B b$$

The elements $p:\sum_{a:A} f(a) =_B b$ are the fibers of the function $f:A \to B$ at element $y:B$.

We could use the type $\sum_{a:A} f(a) =_B b$ wherever we want to get the type of fibers of a function at an element, but it is cumbersome to write out, and we would like to abbreviate that to the type $\mathrm{fiber}_{A, B}(f, y)$. This motivates introducing rules for $\mathrm{fiber}_{A, B}$ types separate from the existing rules for Sigma types:

Formation rules for fiber types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B, y:B, x:A \vdash f(x) =_B y \; \mathrm{type}}{\Gamma, f:A \to B, y:B \vdash \mathrm{fiber}_{A, B}(f, y) \; \mathrm{type}}$$

Introduction rules for fiber types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B, y:B, x:A \vdash b(x):f(x) =_B y \quad \Gamma \vdash a:A \quad \Gamma, f:A \to B, y:B \vdash p:f[a/x] =_B y}{\Gamma, f:A \to B, y:B \vdash (a, b):\mathrm{fiber}_{A, B}(f, y)}$$

Elimination rules for fiber types:

$$\frac{\Gamma, f:A \to B, y:B \vdash z:\mathrm{fiber}_{A, B}(f, y)}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma, f:A \to B, y:B \vdash z:\mathrm{fiber}_{A, B}(f, y)}{\Gamma, f:A \to B, y:B \vdash \pi_2(z):f(\pi_1(z)) =_B y}$$

Computation rules for fiber types:

$$\frac{\Gamma, f:A \to B, y:B, x:A \vdash b(x):f(x) =_B b \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\mathrm{fiber}_{A, B} 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma, f:A \to B, y:B, x:A \vdash b(x):f(x) =_B y \quad \Gamma \vdash a:A}{\Gamma, f:A \to B, y:B \vdash \beta_{\mathrm{fiber}_{A, B} 2}:\pi_2(a, b) =_{f(\pi_1(a, b)) =_B y} b}$$

Uniqueness rules for fiber types:

$$\frac{\Gamma, f:A \to B, y:B \vdash z:\mathrm{fiber}_{A, B}(f, y)}{\Gamma, f:A \to B, y:B \vdash \eta_{\mathrm{fiber}_{A, B}}:z =_{\mathrm{fiber}_{A, B}(f, y)} (\pi_1(z), \pi_2(z))}$$

\subsection{isEquiv types}

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, as the type

$$\prod_{b:B} \mathrm{isContr}(\mathrm{fiber}_{A, B}(f, b)$$

but the name used for such a function in objective type theory is equivalence?, rather than bijection. The elements

$$p:\prod_{b:B} \mathrm{isContr}(\mathrm{fiber}_{A, B}(f, b)$$

are witnesses that the function $f:A \to B$ is an equivalence.

We could use the type

$$\prod_{b:B} \mathrm{isContr}(\mathrm{fiber}_{A, B}(f, b)$$

wherever we want to see if a function $f:A \to B$ is an equivalence, but it is cumbersome to write out, and we would like to abbreviate that to the type $\mathrm{isEquiv}(f)$. This motivates introducing rules for $\mathrm{isEquiv}(f)$ types separate from the existing rules for Pi types:

Formation rules for isEquiv types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B, y:B \vdash \mathrm{isContr}(\mathrm{fiber}_{A, B}(f, y)) \; \mathrm{type}}{\Gamma \vdash \mathrm{isEquiv}_{A, B}(f) \; \mathrm{type}}$$

Introduction rules for isEquiv types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B, y:B \vdash b(y):\mathrm{isContr}(\mathrm{fiber}_{A, B}(f, y))}{\Gamma, f:A \to B \vdash \lambda x.b(x):\mathrm{isEquiv}_{A, B}(f)}$$

Elimination rules for isEquiv types:

$$\frac{\Gamma, f:A \to B \vdash p:\mathrm{isEquiv}_{A, B}(f) \quad \Gamma \vdash c:B}{\Gamma, f:A \to B \vdash p(a):\mathrm{isEquiv}_{A, B}(f)(c)}$$

Computation rules for isEquiv types:

$$\frac{\Gamma, f:A \to B, y:B \vdash b(y):\mathrm{isContr}(\mathrm{fiber}_{A, B}(f, y)) \quad \Gamma \vdash c:B}{\Gamma, f:A \to B \vdash \beta_\mathrm{isEquiv}:\lambda x.b(x)(c) =_{\mathrm{isContr}(\mathrm{fiber}_{A, B}(f, c))} b(c)}$$

Uniqueness rules for isEquiv types:

$$\frac{\Gamma, f:A \to B \vdash p:\mathrm{isEquiv}_{A, B}(f)}{\Gamma, f:A \to B \vdash \eta_\mathrm{isEquiv}:p =_{\mathrm{isEquiv}_{A, B}(f)} \lambda(x).p(x)}$$

\subsection{Equivalence types}

The type of equivalences is given by the type

$$\sum_{f:A \to B} \mathrm{isEquiv}(f)$$

The elements $g:\sum_{f:A \to B} \mathrm{isEquiv}(f)$ are equivalences between $A$ and $B$.

We could use the type $\sum_{f:A \to B} \mathrm{isEquiv}(f)$ wherever we want to get the type of equivalences between two types $A$ and $B$, but it is cumbersome to write out, and we would like to abbreviate that to the type $A \simeq B$. This motivates introducing rules for $A \simeq B$ types separate from the existing rules for Sigma types:

Formation rules for equivalence types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B \vdash \mathrm{isEquiv}(f) \; \mathrm{type}}{\Gamma \vdash A \simeq B \; \mathrm{type}}$$

Introduction rules for equivalence types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B \vdash p(f):\mathrm{isEquiv}(f) \quad \Gamma \vdash g:A \to B \quad \Gamma \vdash p:\mathrm{isEquiv}[g/f]}{\Gamma \vdash (g, p):A \simeq B}$$

Elimination rules for equivalence types:

$$\frac{\Gamma \vdash h:A \simeq B}{\Gamma \vdash \pi_1(h):A \to B} \qquad \frac{\Gamma \vdash h:A \simeq B}{\Gamma \vdash \pi_2(h):\mathrm{isEquiv}(\pi_1(h))}$$

Computation rules for equivalence types:

$$\frac{\Gamma, f:A \to B \vdash p(f):\mathrm{isEquiv}(f) \quad \Gamma \vdash g:A \to B}{\Gamma \vdash \beta_{\simeq 1}:\pi_1(g, p) =_{A \to B} g} \qquad \frac{\Gamma, f:A \to B \vdash p:\mathrm{isEquiv} \quad \Gamma \vdash g:A \to B}{\Gamma \vdash \beta_{\simeq 2}:\pi_2(g, p) =_{\mathrm{isEquiv}(\pi_1(g, p))} p}$$

Uniqueness rules for equivalence types:

$$\frac{\Gamma \vdash h:A \simeq B}{\Gamma \vdash \eta_\simeq:h =_{A \simeq B} (\pi_1(h), \pi_2(h))}$$

\subsection{Definitions of types}

Now that we have equivalences between types, we can finally define types.

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, where we have a derivation

$$\frac{\mathcal{D}}{\Gamma \vdash A \; \mathrm{type}}$$

if we wish to make a definition $B \coloneqq A$, then we can similarly extend the derivation tree with

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash B \coloneqq A \; \mathrm{type}}$$

The effect of such a definition in this case is that we have extended our type theory with a new constant $B$, for which the following inference rules are valid

$$\frac{\mathcal{D}}{B \; \mathrm{type}} \qquad \frac{\mathcal{D}}{\mathrm{defequiv}(B, A): B \simeq A}$$

In essence, we define an element $b$ to be equal to $a$, and a type $B$ to be equivalent to $A$, in the same way that in structural set theory?, which usually also doesn’t have definitional equality, one would define element $b$ to be equal to $a$ and set $B$ to be in bijection? with $A$.

\subsection{Transport}

Transport is the statement that given a type family $P$ indexed by $A$ and elements $a:A$ and $b:A$, there is a function $\mathrm{trans}^P(a, b):(a =_A b) \to (P(a) \simeq P(b))$ from the identity type of $a$ and $b$ to the type of equivalences between the types $P(a)$ and $P(b)$. This is inductively defined on reflexivity on $a:A$, which transport takes to the identity function on $P(a)$, $\mathrm{trans}^P(a, a, \mathrm{refl}_A(a)) =_{P(a) \simeq P(a)} id_{P(a)}$.

Transport is given by the following rules:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash P \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A}{\Gamma \vdash \mathrm{trans}^P(a, b):(a =_A b) \to (P[a/x] \simeq P[b/x])}$$

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash P \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash \mathrm{ind}_{\mathrm{trans}^P}^{\mathrm{refl}}\mathrm{trans}^P(a, a)(\mathrm{refl}_A(a)) =_{P[a/x] \simeq P[a/x]} \mathrm{id}_{P[a/x]}}$$

Transport is very important in defining both univalent Tarski universes? and higher inductive types in objective type theory.

\subsection{Universes}

Universe Universes formation are internal models ofdependent type theory inside of the type theory itself. An universe consists of a type of encodings for types $\mathcal{U}$ and a universal type family $\mathcal{T}$ which takes the encodings and returns an actual type, resulting in the formation and type reflection rules for universes:

$$\frac{\Gamma \mathrm{ctx}}{\Gamma ,x:\mathbb{N}⊢𝒰\mathrm{type}}\frac{\Gamma ⊢A:𝒰}{\Gamma ⊢𝒯(A)\mathrm{type}}$$ \frac{\Gamma \; \mathrm{ctx}}{\Gamma, \mathrm{ctx}}{\Gamma x:\mathbb{N} \vdash \mathcal{U} \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathcal{U}}{\Gamma \vdash \mathcal{T}(A) \; \mathrm{type}}

Hierarchy Given formation an encoding$A:\mathcal{U}$, an internal type family indexed by $A$ is a function $B:\mathcal{T}(A) \to \mathcal{U}$.

$$\frac{\Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathcal{U}[n/x]:\mathcal{U}[s(n)/x]}$$

\subsubsection{Univalence}

Type There reflection are two ways to say that$A:\mathcal{U}$ and $B:\mathcal{U}$ are the same, by way of the identity type of the universe $A =_\mathcal{U} B$, and by way of the type of equivalences between the type reflections of $A:\mathcal{U}$ and $B:\mathcal{U}$, $\mathcal{T}(A) \simeq \mathcal{T}(B)$. By transport, there is a canonical function

$$\frac{\Gamma ,x:\mathbb{N}⊢A:𝒰}{\Gamma ,x:\mathbb{N}⊢A\mathrm{type}}{\mathrm{trans}}^{𝒯}\mathrm{Russell}(A\frac{\Gamma ,x:\mathbb{N}⊢A:𝒰}{\Gamma ,x:\mathbb{N}⊢\mathrm{El}(A)\mathrm{type}},\mathrm{<span><del\; class="diffmod">\; Tarski</del><ins\; class="diffmod">\; B</ins></span>}):(A{=}_{𝒰}B)\to (𝒯(A)\simeq 𝒯(B))$$ \frac{\Gamma, \mathrm{trans}^{\mathcal{T}}(A, x:\mathbb{N} B):(A \vdash =_\mathcal{U} A B) : \to \mathcal{U}}{\Gamma, (\mathcal{T}(A) x:\mathbb{N} \simeq \vdash \mathcal{T}(B)) A \; \mathrm{type}}\mathrm{Russell} \qquad \frac{\Gamma, x:\mathbb{N} \vdash A : \mathcal{U}}{\Gamma, x:\mathbb{N} \vdash \mathrm{El}(A) \; \mathrm{type}}\mathrm{Tarski}

Lifting The universe$\mathcal{U}$ is then said to be a univalent universe if the transport function $\mathrm{trans}^{\mathcal{T}}(A, B)$ is an equivalence of types

$$\frac{\Gamma ,x:\mathbb{N}⊢A:𝒰}{\Gamma ,x:\mathbb{N}⊢A[s(x)/x]:𝒰[s(x)/x]}\mathrm{univalence}(A,B):\mathrm{isEquiv}({\mathrm{trans}}^{𝒯}(A,B))$$ \frac{\Gamma, \mathrm{univalence}(A, x:\mathbb{N} B):\mathrm{isEquiv}(\mathrm{trans}^{\mathcal{T}}(A, \vdash B)) A : \mathcal{U}}{\Gamma, x:\mathbb{N} \vdash A[s(x)/x] : \mathcal{U}[s(x)/x]}

Univalence for all encodings$A:\mathcal{U}$ and $B:\mathcal{U}$. This is given by the following rule

$$\frac{\Gamma <span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; ⊢</ins></span>\mathrm{<span><del\; class="diffmod">\; x</del><ins\; class="diffmod">\; A</ins></span>}:\mathrm{<span><del\; class="diffmod">\; \mathbb{N}</del><ins\; class="diffmod">\; 𝒰</ins></span>}\Gamma ⊢B:𝒰\mathrm{type}}{\Gamma ,x:\mathbb{N},A:𝒰,B:𝒰⊢\mathrm{<span><del\; class="diffmod">\; ua</del><ins\; class="diffmod">\; univalence</ins></span>}:(A{=}_{𝒰},B){\simeq }_{𝒰[s(x)/x]}:\mathrm{isEquiv}({\mathrm{trans}}^{𝒯}(A{\simeq }_{𝒰},B))}$$ \frac{\Gamma, \frac{\Gamma x:\mathbb{N} \vdash \mathcal{U} A:\mathcal{U} \; \quad \mathrm{type}}{\Gamma, \Gamma x:\mathbb{N}, A:\mathcal{U}, B:\mathcal{U} \vdash \mathrm{ua}:(A B:\mathcal{U}}{\Gamma =_\mathcal{U} \vdash B) \mathrm{univalence}(A, \simeq_{\mathcal{U}[s(x)/x]} B):\mathrm{isEquiv}(\mathrm{trans}^{\mathcal{T}}(A, (A B))} \simeq_\mathcal{U} B)}

Universes are usually also required to be closed under all the type formers introduced previously.

\subsubsection{Internal identity types}

A universe $\mathcal{U}$ is closed under identity types if it has an internal encoding of identity types in the universe: Given an element $A:\mathcal{U}$, there is a function $\mathrm{Id}^\mathcal{U}(A):\mathcal{T}(A) \times \mathcal{T}(A) \to \mathcal{U}$ and for all elements $a:\mathcal{T}(A)$ and $b:\mathcal{T}(A)$ an equivalence

$$\mathrm{canonical}_{\mathrm{Id}}^{\mathcal{U}}(A)(a, b):\mathcal{T}(\mathrm{Id}^\mathcal{U}(A)(a, b)) \simeq (a =_{\mathcal{T}(A)} b)$$

The rules for the internal identity types are thus given by

$$\frac{\Gamma \vdash A:\mathcal{U}}{\Gamma \vdash \mathrm{Id}^\mathcal{U}(A):\mathcal{T}(A) \times \mathcal{T}(A) \to \mathcal{U}} \qquad \frac{\Gamma \vdash A:\mathcal{U} \quad \Gamma \vdash a:\mathcal{T}(A) \quad \Gamma \vdash b:\mathcal{T}(A)}{\Gamma \vdash \mathrm{canonical}_{\mathrm{Id}}^{\mathcal{U}}(A)(a, b):\mathcal{T}(\mathrm{Id}^\mathcal{U}(A)(a, b)) \simeq (a =_{\mathcal{T}(A)} b)}$$

\subsubsection{Internal function types}

A universe $\mathcal{U}$ is closed under function types if it has an internal encoding of function types in the universe: given an element $A:\mathcal{U}$ and an element $B:\mathcal{U}$, there is an element $A \to_\mathcal{U} B:\mathcal{U}$, and an equivalence

$$\mathrm{canonical}_{\to}^{\mathcal{U}}(A, B):\mathcal{T}(A \to_\mathcal{U} B) \simeq \mathcal{T}(A) \to \mathcal{T}(B)$$

The rules for the internal function types are thus given by

$$\frac{\Gamma \vdash A:\mathcal{U} \quad \Gamma \vdash B:\mathcal{U}}{\Gamma \vdash A \to_\mathcal{U} B:\mathcal{U}} \qquad \frac{\Gamma \vdash A:\mathcal{U} \quad \Gamma \vdash B:\mathcal{U}}{\Gamma \vdash \mathrm{canonical}_{\to}^{\mathcal{U}}(A, B):\mathcal{T}(A \to_\mathcal{U} B) \simeq \mathcal{T}(A) \to \mathcal{T}(B)}$$

\subsubsection{Internal pi types}

A universe $\mathcal{U}$ is closed under pi types if it has an internal encoding of pi types in the universe: given an element $A:\mathcal{U}$ and a function $B:\mathcal{T}(A) \to \mathcal{U}$, there is an element $\Pi_\mathcal{U}(x:A).B(x):\mathcal{U}$, and an equivalence

$$\mathrm{canonical}_\Pi^{\mathcal{U}}(A, B):\mathcal{T}(\Pi_\mathcal{U}(x:A).B(x)) \simeq \prod_{x:\mathcal{T}(A)} \mathcal{T}(B(x))$$

The rules for the internal pi types are thus given by

$$\frac{\Gamma \vdash A:\mathcal{U} \quad \Gamma \vdash B:\mathcal{T}(A) \to \mathcal{U}}{\Gamma \vdash \Pi_\mathcal{U}(x:A).B(x):\mathcal{U}} \qquad \frac{\Gamma \vdash A:\mathcal{U} \quad \Gamma \vdash B:\mathcal{T}(A) \to \mathcal{U}}{\Gamma \vdash \mathrm{canonical}_\Pi^{\mathcal{U}}(A, B):\mathcal{T}(\Pi_\mathcal{U}(x:A).B(x)) \simeq \prod_{x:\mathcal{T}(A)} \mathcal{T}(B(x))}$$

\subsubsection{Internal product types}

A universe $\mathcal{U}$ is closed under product types if it has an internal encoding of product types in the universe: given an element $A:\mathcal{U}$ and an element $B:\mathcal{U}$, there is an element $A \times_\mathcal{U} B:\mathcal{U}$, and an equivalence

$$\mathrm{canonical}_{\times}^{\mathcal{U}}(A, B):\mathcal{T}(A \times_\mathcal{U} B) \simeq \mathcal{T}(A) \times \mathcal{T}(B)$$

The rules for the internal product types are thus given by

$$\frac{\Gamma \vdash A:\mathcal{U} \quad \Gamma \vdash B:\mathcal{U}}{\Gamma \vdash A \times_\mathcal{U} B:\mathcal{U}} \qquad \frac{\Gamma \vdash A:\mathcal{U} \quad \Gamma \vdash B:\mathcal{U}}{\Gamma \vdash \mathrm{canonical}_{\imes}^{\mathcal{U}}(A, B):\mathcal{T}(A \times_\mathcal{U} B) \simeq \mathcal{T}(A) \times \mathcal{T}(B)}$$

\subsubsection{Internal sigma types}

A universe $\mathcal{U}$ is closed under sigma types if it has an internal encoding of sigma types in the universe: given an element $A:\mathcal{U}$ and a function $B:\mathcal{T}(A) \to \mathcal{U}$, there is an element $\Sigma_\mathcal{U}(x:A).B(x):\mathcal{U}$, and an equivalence

$$\mathrm{canonical}_\Sigma^{\mathcal{U}}(A, B):\mathcal{T}(\Sigma_\mathcal{U}(x:A).B(x)) \simeq \sum_{x:\mathcal{T}(A)} \mathcal{T}(B(x))$$

The rules for the internal sigma types are thus given by

$$\frac{\Gamma \vdash A:\mathcal{U} \quad \Gamma \vdash B:\mathcal{T}(A) \to \mathcal{U}}{\Gamma \vdash \Sigma_\mathcal{U}(x:A).B(x):\mathcal{U}} \qquad \frac{\Gamma \vdash A:\mathcal{U} \quad \Gamma \vdash B:\mathcal{T}(A) \to \mathcal{U}}{\Gamma \vdash \mathrm{canonical}_\Sigma^{\mathcal{U}}(A, B):\mathcal{T}(\Pi_\mathcal{U}(x:A).B(x)) \simeq \sum_{x:\mathcal{T}(A)} \mathcal{T}(B(x))}$$

\subsubsection{Internal sum types}

A universe $\mathcal{U}$ is closed under sum types if it has an internal encoding of sum types in the universe: given an element $A:\mathcal{U}$ and an element $B:\mathcal{U}$, there is an element $A +_\mathcal{U} B:\mathcal{U}$, and an equivalence

$$\mathrm{canonical}_{+}^{\mathcal{U}}(A, B):\mathcal{T}(A +_\mathcal{U} B) \simeq \mathcal{T}(A) + \mathcal{T}(B)$$

The rules for the internal sum types are thus given by

$$\frac{\Gamma \vdash A:\mathcal{U} \quad \Gamma \vdash B:\mathcal{U}}{\Gamma \vdash A +_\mathcal{U} B:\mathcal{U}} \qquad \frac{\Gamma \vdash A:\mathcal{U} \quad \Gamma \vdash B:\mathcal{U}}{\Gamma \vdash \mathrm{canonical}_{+}^{\mathcal{U}}(A, B):\mathcal{T}(A +_\mathcal{U} B) \simeq \mathcal{T}(A) + \mathcal{T}(B)}$$

\subsubsection{Internal empty type}

A universe $\mathcal{U}$ is closed under the empty type if it has an internal encoding of the empty type in the universe: there is an element $\mathbb{0}_\mathcal{U}:\mathcal{U}$, and an equivalence

$$\mathrm{canonical}_{\mathbb{0}}^{\mathcal{U}}:\mathcal{T}(\mathbb{0}_\mathcal{U}) \simeq \mathbb{0}$$

The rules for the internal empty type are thus given by

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{0}_\mathcal{U}:\mathcal{U}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{canonical}_{\mathbb{0}}^{\mathcal{U}}:\mathcal{T}(\mathbb{0}_\mathcal{U}) \simeq \mathbb{0}}$$

\subsubsection{Internal unit type}

A universe $\mathcal{U}$ is closed under the unit type if it has an internal encoding of the unit type in the universe: there is an element $\mathbb{1}_\mathcal{U}:\mathcal{U}$, and an equivalence

$$\mathrm{canonical}_{\mathbb{1}}^{\mathcal{U}}:\mathcal{T}(\mathbb{1}_\mathcal{U}) \simeq \mathbb{1}$$

The rules for the internal unit type are thus given by

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{1}_\mathcal{U}:\mathcal{U}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{canonical}_{\mathbb{1}}^{\mathcal{U}}:\mathcal{T}(\mathbb{1}_\mathcal{U}) \simeq \mathbb{1}}$$

\subsubsection{Internal booleans type}

A universe $\mathcal{U}$ is closed under the booleans type if it has an internal encoding of the booleans type in the universe: there is an element $\mathbb{2}_\mathcal{U}:\mathcal{U}$, and an equivalence

$$\mathrm{canonical}_{\mathbb{2}}^{\mathcal{U}}:\mathcal{T}(\mathbb{2}_\mathcal{U}) \simeq \mathbb{2}$$

The rules for the internal booleans type are thus given by

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{2}_\mathcal{U}:\mathcal{U}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{canonical}_{\mathbb{2}}^{\mathcal{U}}:\mathcal{T}(\mathbb{2}_\mathcal{U}) \simeq \mathbb{2}}$$

\subsubsection{Internal natural numbers type}

A universe $\mathcal{U}$ is closed under the natural numbers type if it has an internal encoding of the natural numbers type in the universe: there is an element $\mathbb{N}_\mathcal{U}:\mathcal{U}$, and an equivalence

$$\mathrm{canonical}_{\mathbb{N}}^{\mathcal{U}}:\mathcal{T}(\mathbb{N}_\mathcal{U}) \simeq \mathbb{N}$$

The rules for the internal natural numbers type are thus given by

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N}_\mathcal{U}:\mathcal{U}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{canonical}_{\mathbb{N}}^{\mathcal{U}}:\mathcal{T}(\mathbb{N}_\mathcal{U}) \simeq \mathbb{N}}$$

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

• dependent type theory
• cohesive homotopy type theory

\section{External links}

• the nLab’s article on homotopy type theory

category: redirected to nlab