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

Showing changes from revision #16 to #17: 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

• univalent univalence universes

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

In a similar manner, for simplicity and ease of presentation, we shall also avoid follow the HoTT use book of in universes, not and including have a separate single$A \; \mathrm{type}$ judgment and rather stipulating that every type is an element additional of type a former Russell universe.$A = B$ for equality of types. This allows us to express univalence as a rule in the type theory, without having to define universes.

Universes are relegated to a discussion of cardinals and size issues in various branches of mathematics, such as in order theory, category theory, set theory, and model theory, and won’t be described here.

\subsection{Judgments and contexts}

We Objective introduce type two theory consists of three judgments: type judgments in the model: typing judgments, where we judge$\mathrm{<span><del\; class="diffmod">\; a</del><ins\; class="diffmod">\; A</ins></span>}\mathrm{type}$ a A \; \mathrm{type} , to where be we an judge element of$A$ , to be a type, typing judgments, where we judge$a:A$ a:A a , and to context be judgments, an where element we of judge$\mathrm{<span><del\; class="diffmod">\; \Gamma </del><ins\; class="diffmod">\; A</ins></span>}$ \Gamma A , to be a context,$\mathrm{<span><del\; class="diffmod">\; \Gamma </del><ins\; class="diffmod">\; a</ins></span>}:\mathrm{<span><del\; class="diffmod">\; ctx</del><ins\; class="diffmod">\; A</ins></span>}$ \Gamma a:A \; \mathrm{ctx} . , Contexts and are context lists judgments, of where typing we judgments judge$\mathrm{<span><del\; class="diffmod">\; a</del><ins\; class="diffmod">\; \Gamma </ins></span>}:A$ a:A \Gamma , to be a context,$\mathrm{<span><del\; class="diffmod">\; b</del><ins\; class="diffmod">\; \Gamma </ins></span>}:\mathrm{<span><del\; class="diffmod">\; B</del><ins\; class="diffmod">\; ctx</ins></span>}$ b:B \Gamma \; \mathrm{ctx} , . Contexts are lists of typing judgments$\mathrm{<span><del\; class="diffmod">\; c</del><ins\; class="diffmod">\; a</ins></span>}:\mathrm{<span><del\; class="diffmod">\; C</del><ins\; class="diffmod">\; A</ins></span>}$ c:C 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{Russell \subsection{Dependent universes} types and sections}

Universes A are dependent the types of types in type theory. 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$.

We A introduce section or dependent term is a hierarchy term of universes$U_{i}b:B$ U_i b:B indexed in by the natural context numbers of the variable judgment$\mathrm{<span><del\; class="diffmod">\; i</del><ins\; class="diffmod">\; x</ins></span>}:A$ i x:A , in the metatheory, with rules for universe formation and cumulativity.$x:A \vdash b:B$. Sections are likewise usually written as $b(x)$ to indicate its dependence upon $x$.

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash U_i : U_{i + 1}} \qquad \frac{\Gamma \vdash A:U_i}{\Gamma \vdash A:U_{i + 1}}$$

\subsection{Equality of elements}

\subsection{Sections Equality and of dependent elements types} of a type in objective type theory is represented by a type known as theequality type or the type of equalities. The elements of the equality type are called equalities.

A Equality section of is elements comes with a term formation rule, an introduction rule, an elimination rule, and a computation rule:$b:B$ in the context of the variable judgment $x:A$, $x:A \vdash b:B$. Sections are usually written as $b(x)$ to indicate its dependence upon $x$.

A Formation dependent rule type for is equality a types section of a elements: universe$B:U_i$ in the context of the variable judgment $x:A$, $x:A \vdash B:U_i$, and since they are sections, they are usually written as $B(x)$.

\subsection{Equality}

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

Equality Introduction in rule type for theory equality is types represented by the identity type, which is also called the path type or identification type. The terms of the elements: identity type could be called paths or identifications.

Equality comes with a formation rule, an introduction rule, an elimination rule, and a computation rule:

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

Formation Elimination rule for identity equality types: types of elements:

$$\frac{\Gamma ,a:A,b:A,p:a{=}_{A}b⊢C(a,b,p)\mathrm{type}\Gamma ,a:A⊢t:U_{i}C(a,a,{\mathrm{refl}}_A(a))}{\Gamma ,a:A,b:A<span><del\; class="diffmod">\; ⊢</del><ins\; class="diffmod">\; ,</ins></span>p:a{=}_{A}b⊢J(t,a,b,p):U_{i}C(a,b,p)}$$ \frac{\Gamma \frac{\Gamma, \vdash A:U_i}{\Gamma, a:A, b:A b:A, p:a =_A b \vdash a 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:U_i} b \vdash J(t, a, b, p):C(a, b, p)}

Introduction Computation rule rules for identity equality types: types of elements:

$$\frac{\Gamma ,a:A,b:A,p:a{=}_{A}b⊢C(a,b,p)\mathrm{type}\Gamma ,a:A⊢t:U_{i}C(a,a,{\mathrm{refl}}_A(a))}{\Gamma ,a:A,b:A,p:a{=}_{A}b⊢{\mathrm{<span><del\; class="diffmod">\; refl</del><ins\; class="diffmod">\; \beta </ins></span>}}_A(a):J(t,a{=}_A,a,\mathrm{refl}(a)){=}_{C(a,a,{\mathrm{refl}}_A(a))}t}$$ \frac{\Gamma \frac{\Gamma, a:A, b:A, p:a =_A b \vdash A:U_i}{\Gamma, C(a, b, p) \; \mathrm{type} \quad \Gamma, a:A \vdash \mathrm{refl}_A(a) t:C(a, : a, a \mathrm{refl}_A(a))}{\Gamma, a:A, b:A, p:a =_A a} b \vdash \beta_{=_A}(a) : J(t, a, a, \mathrm{refl}(a)) =_{C(a, a, \mathrm{refl}_A(a))} t}

Elimination \subsection{Equality rule of for types} identity types:

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

Equality of types is also an identity type, represented by the bare equality symbol $A = B$ for types $A$ and $B$. As types do not belong to any type, the rules for the equality types of types is slightly different from the rules for the equality types of terms:

Computation Type rules formation for identity equality of types:

$$\frac{\Gamma ,a:A,b:A,p:a{=}_{A}b,\Delta (a,b,p)⊢\mathrm{<span><del\; class="diffmod">\; C</del><ins\; class="diffmod">\; A</ins></span>}(\mathrm{<span><del\; class="diffmod">\; a</del><ins\; class="diffmod">\; type</ins></span>},b,p):U_i\Gamma ,a:A,\Delta (a,a,{\mathrm{refl}}_A(a))⊢\mathrm{<span><del\; class="diffmod">\; t</del><ins\; class="diffmod">\; B</ins></span>}:\mathrm{<span><del\; class="diffmod">\; C</del><ins\; class="diffmod">\; type</ins></span>}(a,a,{\mathrm{refl}}_A(a))}{\Gamma ,a:A,b:A,p:a{=}_{A}b,\Delta (a,b,p)⊢{\beta }_{{=}_A}A<span><del\; class="diffmod">\; (</del><ins\; class="diffmod">\; =</ins></span>\mathrm{<span><del\; class="diffmod">\; a</del><ins\; class="diffmod">\; B</ins></span>}):\mathrm{type}J(t,a,a,\mathrm{refl}(a)){=}_{C(a,a,{\mathrm{refl}}_A(a))}t}$$ \frac{\Gamma, \frac{\Gamma a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash C(a, A b, \; p):U_i \mathrm{type} \quad \Gamma, \Gamma a:A, \Delta(a, a, \mathrm{refl}_A(a)) \vdash t:C(a, B a, \; \mathrm{refl}_A(a))}{\Gamma, \mathrm{type}}{\Gamma a:A, b:A, p:a =_A b, \Delta(a, b, p) \vdash \beta_{=_A}(a) A : = J(t, B a, \; a, \mathrm{type}} \mathrm{refl}(a)) =_{C(a, a, \mathrm{refl}_A(a))} t}

The type formation rule for equality types states that given the hypothesis that $A$ and $B$ are types in context $\Gamma$, one could form the conclusion that in the contexts of $\Gamma$ one could form the equality type $A = B$.

Element introduction for equality of types:

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{refl}_A : A = A}$$

The element introduction rule for equality types states that given the hypothesis that $A$ is a type in context $\Gamma$, one could form the conclusion that in the contexts of $\Gamma$ one could introduce the element $\mathrm{refl}_A : A = A$, called reflexivity.

Element elimination for equality of types:

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

This says that given

Conversion rules for equality of types:

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

\subsection{Definitions}

In mathematics, many times one would want to define an element to be another element of a type. In order to define an element $a:A$ to be an element $b:A$, one says that element $a:A$ comes with an identification equality$\mathrm{def}(a,b):a{=}_{A}b$ \mathrm{def}(a):a \mathrm{def}(a, b):a =_A b . Since Similarly, types are elements of universes, one defines a type$A:{𝒰}_i$ A:\mathcal{U}_i A to be a type $B:{𝒰}_i$ B:\mathcal{U}_i B if the type $A:{𝒰}_i$ A:\mathcal{U}_i A comes with an identification equality$\mathrm{def}(A,B):A{=}_{{𝒰}_i}=B$ \mathrm{def}(A):A \mathrm{def}(A, =_{\mathcal{U}_i} B):A = B . This is formalized with the initialization operator$\coloneqq$ by the following rules for definitions of terms

Sometimes, for ease of simplicity, the identity type is simply written $a = b$ for elements $a:A$ and $b:A$. The type argument $A$ for the identity type then becomes an implicit argument. Thus, in order to define $a$ to be $b$, one says that $a$ comes with an identification $\mathrm{def}(a):a = b$.

$$\frac{\Gamma \vdash a:A}{\Gamma \vdash b \coloneqq a:A} \qquad \frac{\Gamma \vdash b \coloneqq a:A}{\Gamma \vdash b:A} \qquad \frac{\Gamma \vdash b \coloneqq a:A}{\Gamma \vdash \mathrm{def}(a, b):b =_A a}$$

In and a similarly proof for assistant definitions or of some types other program,elaboration is needed to expand out all the implicit arguments to get the right type $a =_A b$.

\subsection{Natural numbers}

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash B \coloneqq A \; \mathrm{type}} \qquad \frac{\Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma \vdash B \; \mathrm{type}} \qquad \frac{\Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma \vdash \mathrm{def}_{A, B}:B = A}$$

Formation rules for the natural numbers:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N}:U_i}$$

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(x):U_i \quad \Gamma \vdash c_0:C(0) \quad \Gamma, x:\mathbb{N}, c(x):C(x) \vdash c_s(x, c(x)):C(s(x)) \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{ind}_C^n(c_0, c_s):C(n)}$$

Computation rules for the natural numbers:

$$\frac{\Gamma, x:\mathbb{N} \vdash C(x):U_i \quad \Gamma \vdash c_0:C(0) \quad \Gamma, x:\mathbb{N}, c(x):C(x) \vdash c_s(x, c(x)):C(s(x))}{\Gamma \vdash \beta_\mathrm{N}^{0}: \mathrm{ind}_C^0(c_0, c_s) =_{C(0)} c_0}$$

$$\frac{\Gamma, x:\mathbb{N} \vdash C(x):U_i \quad \Gamma \vdash c_0:C(0) \quad \Gamma, x:\mathbb{N}, c(x):C(x) \vdash c_s(x, c(x)):C(s(x))}{\Gamma \vdash \beta_\mathrm{N}^{s}: \mathrm{ind}_C^{s(n)}(c_0, c_s) =_{C(s(n))} c_s(n, \mathrm{ind}_C^{n}(c_0, c_s))}$$

Uniqueness rules for the natural numbers: …

\subsection{Function types}

Formation rules for function types:

$$\frac{\Gamma ⊢A:U_i\mathrm{type}\Gamma ⊢B:U_i\mathrm{type}}{\Gamma ⊢A\to B:U_i\mathrm{type}}$$ \frac{\Gamma \vdash A:U_i A \; \mathrm{type} \quad \Gamma \vdash B:U_i}{\Gamma B \; \mathrm{type}}{\Gamma \vdash A \to B:U_i} 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{Pi types}

Pi types are the dependent versions of functions or products, depending on how one looks at it.

Formation rules for Pi types:

$$\frac{\Gamma ⊢A:U_i\mathrm{type}\Gamma ,x:A⊢B(x):U_i\mathrm{type}}{\Gamma ⊢\Pi \prod _{x:A}(x:A).B(x):U_i\mathrm{type}}$$ \frac{\Gamma \vdash A:U_i A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x):U_i}{\Gamma B(x) \; \mathrm{type}}{\Gamma \vdash \Pi(x:A).B(x):U_i} \prod_{x:A} B(x) \; \mathrm{type}}

Introduction rules for Pi types:

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

Elimination rules for Pi types:

$$\frac{\Gamma ⊢f:\Pi \prod (x:Ax:A).B(x)\Gamma ⊢a:A}{\Gamma ⊢f(a):B[a/x]}$$ \frac{\Gamma \vdash f:\Pi(x:A).B(x) 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 ⊢f:\Pi \prod _{x:A}(x:A).B(x)}{\Gamma ⊢{\eta }_{\Pi }:f{=}_{\Pi \prod _{x:A}(x:A).B(x)}\lambda (x).f(x)}$$ \frac{\Gamma \vdash f:\Pi(x:A).B(x)}{\Gamma f:\prod_{x:A} B(x)}{\Gamma \vdash \eta_\Pi:f =_{\Pi(x:A).B(x)} =_{\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 ⊢A:U_i\mathrm{type}\Gamma ⊢B:U_i\mathrm{type}}{\Gamma ⊢A\times B:U_i\mathrm{type}}$$ \frac{\Gamma \vdash A:U_i A \; \mathrm{type} \quad \Gamma \vdash B:U_i}{\Gamma B \; \mathrm{type}}{\Gamma \vdash A \times B:U_i} 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 ⊢a:A\Gamma ⊢b:B}{\Gamma ⊢{\beta }_{\Sigma \times 1}:{\pi }_1(a,b){=}_{A}a}\frac{\Gamma ⊢a:A\Gamma ⊢b:B}{\Gamma ⊢{\beta }_{\Sigma \times 2}:{\pi }_2(a,b){=}_{B}b}$$ \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash \beta_{\Sigma \beta_{\times 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash \beta_{\Sigma \beta_{\times 2}:\pi_2(a, b) =_B b}

Uniqueness rules for product types:

$$\frac{\Gamma ⊢z:A\times B}{\Gamma ⊢{\eta }_{\Sigma }:z{=}_{A\times B}({\pi }_1(z),{\pi }_2(z))}$$ \frac{\Gamma \vdash z:A \times B}{\Gamma \vdash \eta_\Sigma:z \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 ⊢A:U_i\mathrm{type}\Gamma ,x:A⊢B(x):U_i\mathrm{type}}{\Gamma ⊢\Sigma \sum _{x:A}(x:A).B(x):U_i\mathrm{type}}$$ \frac{\Gamma \vdash A:U_i A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x):U_i}{\Gamma B(x) \; \mathrm{type}}{\Gamma \vdash \Sigma(x:A).B(x):U_i} \sum_{x:A} B(x) \; \mathrm{type}}

Introduction rules for Sigma types:

$$\frac{\Gamma ,x:A⊢b(x):B(x)\Gamma ⊢a:A\Gamma ⊢b:B[a/x]}{\Gamma ⊢(a,b):\Sigma \sum _{x:A}(x:A).B(x)}$$ \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):\Sigma(x:A).B(x)} b):\sum_{x:A} B(x)}

Elimination rules for Sigma types:

$$\frac{\Gamma ⊢z:\Sigma \sum _{x:A}(x:A).B(x)}{\Gamma ⊢{\pi }_1(z):A}\frac{\Gamma ⊢z:\Sigma \sum _{x:A}(x:A).B(x)}{\Gamma ⊢{\pi }_2(z):B({\pi }_1(z))}$$ \frac{\Gamma \vdash z:\Sigma(x:A).B(x)}{\Gamma z:\sum_{x:A} B(x)}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:\Sigma(x:A).B(x)}{\Gamma 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 ⊢z:\Sigma \sum _{x:A}(x:A).B(x)}{\Gamma ⊢{\eta }_{\Sigma }:z{=}_{\Sigma \sum _{x:A}(x:A).B(x)}({\pi }_1(z),{\pi }_2(z))}$$ \frac{\Gamma \vdash z:\Sigma(x:A).B(x)}{\Gamma z:\sum_{x:A} B(x)}{\Gamma \vdash \eta_\Sigma:z =_{\Sigma(x:A).B(x)} =_{\sum_{x:A} B(x)} (\pi_1(z), \pi_2(z))}

\subsection{Sum types}

\subsection{Empty type}

\subsection{Unit type}

\subsection{Boolean type}

\subsection{Interval type}

\subsection{Function extensionality}

\subsection{Singletons}

A singleton is a type with only one element up to identifications.

We define the function $\mathrm{isSingl}:U_i \to U_i$ which states that a type $A:U_i$ is a singleton if there is an identification

$$\mathrm{def}(\mathrm{isSingl})(A):\mathrm{isSingl}(A) =_{U_i} \Sigma(a:A).\Pi(b:A).a =_A b$$

\subsection{Fibers}

Given types $A:U_i$ and $B:U_i$ let the type family

$$\mathrm{fiber}(A, B):((A \to B) \times B) \to U_i$$

comes with identifications

$$\mathrm{def}(\mathrm{fiber}(A, B))(f, b):\mathrm{fiber}(A, B)(f, b) =_{U_i} \Sigma(a:A).f(a) =_B b$$

for each function $f:A \to B$ and element $b:B$. The type $\mathrm{fiber}(A, B)(f, b)$ is known as the fiber of $f$ at $b$.

\subsection{Equivalences}

We In define set the theory, type a family set is a$(-)\simeq_{U_i}(-):(U_i \times U_i) \to U_i$pointed set? such if that it comes has with at identifications least one chosen element; it is asubsingleton? if it has at most one element up to equality: every two elements in the set are equal to each other, and it is a singleton? if it has exactly one element up to equality: it is a pointed set and a singleton.

$$\mathrm{def}(\simeq_{U_i})(A, B): (A \simeq_{U_i} B) =_{U_i} \Sigma(f:A \to B).\Pi(b:B).\mathrm{isSingl}(\mathrm{fiber}(A, B)(f, b))$$

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 subsingleton if for every two elements $a:T$ and $b:T$, there is an identification? $f(a, b):a =_T b$, or equivalently, there is a dependent function

for all types $A:U_i$ and $B:U_i$. The type $A \simeq_{U_i} B$ is known as the type of equivalences between $A$ and $B$.

$$f:\prod_{a:T} \prod_{b:T} a =_T b$$

and a type $T$ is a singleton if it has both an element $p:T$ and a dependent function

$$f:\prod_{a:T} \prod_{b:T} a =_T b$$

or equivalently, an element

$$c:T \times \prod_{a:T} \prod_{b:T} a =_T b$$

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

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 $f:A \to B$ is an equivalence if there is an element

$$c(f):\prod_{b:B} \left(\sum_{a:A} f(a) =_B b \right) \times \prod_{p:\sum_{a:A} f(a) =_B b} \prod_{q:\sum_{a:A} f(a) =_B b} p =_{\sum_{a:A} f(a) =_B b} q$$

The type of equivalences is given by

$$\sum_{f:A \to B} \prod_{b:B} \left(\sum_{a:A} f(a) =_B b \right) \times \prod_{p:\sum_{a:A} f(a) =_B b} \prod_{q:\sum_{a:A} f(a) =_B b} p =_{\sum_{a:A} f(a) =_B b} q$$

\subsection{Univalence}

For types $A$ and $B$ there is a function

$$\mathrm{idtoequiv}_{A, B}:(A = B) \to (A \simeq B)$$

inducively defined by

$$\mathrm{def}(\mathrm{idtoequiv}_{A, A}):\mathrm{idtoequiv}_{A, A}(\mathrm{refl}_A) =_{A \simeq A} \mathrm{id}_A$$

Univalence is the statement that one could form the witness that $\mathrm{idtoequiv}_{A, B}$ is an equivalence given types $A$ and $B$, and is given by the rule

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{univalence}_{A, B}:\mathrm{isEquiv}(\mathrm{idtoequiv}_{A, B})}$$

Thus, $(A = B) \simeq (A \simeq B)$, and by univalence again, $(A = B) = (A \simeq B)$.

\subsection{Function extensionality}

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

\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{External links}

• the nLab’s article on homotopy type theory

category: redirected to nlab