1 Syntax of HoTT0

For HoTT, most of the rules are standard. Here, we will go over them.

The Context Rules

\[ {\leavevmode \hbox{ \bottomAlignProof \AxiomC {} \UnaryInfC {$ \epsilon \text{ ctx}$} \DisplayProof } \]

$\Gamma \text{ ctx}$ $\Gamma \vdash A \text{ type}$ $ \Gamma , x : A \text{ ctx}$ $\Gamma , x:A \text{ ctx}$ $\Gamma , x:A \vdash x:A$ $\Gamma , x:A \text{ ctx}$ $\Gamma \vdash y : B$ $\Gamma , x:A \vdash y:B$

\[ \]

The Pi Rules

\[ {\leavevmode \hbox{ \AxiomC {$\Gamma , x:A \vdash B(x) \text{ type}$} \UnaryInfC {$\Gamma \vdash \prod _{a : A} B(a) \text{ type}$} \DisplayProof } \]

$\Gamma , x :A \vdash b(x) : B(x)$ $\Gamma \vdash \lambda (a : A).b(a) : \prod _{a :A} B(a) $

\[ \]

\[ {\leavevmode \hbox{ \AxiomC {$\Gamma \vdash f: \prod _{a :A} B(a)$} \AxiomC {$\Gamma \vdash x : A$} \BinaryInfC {$f(x) : B(x)$} \DisplayProof } \]

$\Gamma , x: A \vdash b(x) : B(x)$ $\Gamma , a:A\vdash \lambda (x: A).b(x)(a) \equiv b(a) : B(a)$

\[ \]

The Sigma Rules

\[ {\leavevmode \hbox{ \AxiomC {$\Gamma , x:A \vdash B(x) \text{ type}$} \UnaryInfC {$\Gamma \vdash \sum _{a : A} B(a) \text{ type}$} \DisplayProof } \]

$\Gamma \vdash a : A$ $\Gamma \vdash b : B(a)$ $\Gamma \vdash \langle a,b\rangle : \sum _{x :A} B(x) $

\[ \]

\[ {\leavevmode \hbox{ \AxiomC {$\Gamma \vdash p: \sum _{x :A} B(x)$} \UnaryInfC {$\Gamma \vdash \text{fst}(p) : A$} \DisplayProof } \]

$\Gamma \vdash p: \sum _{x :A} B(x)$ $\Gamma \vdash \text{snd}(p) : B(\text{fst}(p))$

\[ \]

\[ {\leavevmode \hbox{ \AxiomC {$\Gamma \vdash a : A$} \AxiomC {$\Gamma \vdash b : B(a)$} \BinaryInfC {$\Gamma \vdash \text{fst}(\langle a,b\rangle ) \equiv a : A $} \DisplayProof } \]

$\Gamma \vdash a : A$ $\Gamma \vdash b : B(a)$ $\Gamma \vdash \text{snd}(\langle a,b\rangle ) \equiv b : B(a) $

\[ \]

The Id Rules

\[ {\leavevmode \hbox{ \AxiomC {$\Gamma \vdash a:A$} \AxiomC {$\Gamma \vdash b:A$} \BinaryInfC {$\Gamma \vdash \text{id}_{A}(a,b) \text{ type}$} \DisplayProof } \]

$\Gamma \vdash a:A$ $\Gamma \vdash \text{refl}(a) : \text{id}_{A}(a,a)$

\[ \]

\[ {\leavevmode \hbox{ \AxiomC {$\Gamma ,x:A,y:A,u: \text{id}_A(x,y) \vdash E(x,y,u) \text{ type}$} \AxiomC {$\Gamma , x : A \vdash e(x) : E(x,x,\text{refl}(x))$} \BinaryInfC {$\Gamma ,x:A,y:A,u: \text{id}_A(x,y) \vdash \text{J}(x,y,u,e) : E(x,y,u)$} \DisplayProof } \]

\[ \]

The Universe

\[ {\leavevmode \hbox{ \AxiomC {$\Gamma \text{ ctx}$} \UnaryInfC {$\Gamma \vdash \text{U} \text{ type}$} \DisplayProof } \]

$\Gamma \vdash a : \text{U}$ $\Gamma \vdash \text{El}(a) \text{ type}$

\[ \]

\[ {\leavevmode \hbox{ \AxiomC {$\Gamma ,a : \text{U}, x:\text{El}(a) \vdash b(x) : \text{U}$} \UnaryInfC {$\Gamma ,a : \text{U} \vdash \pi (a,b(x)) : \text{U}$} \DisplayProof } \]

$\Gamma ,a : \text{U}, x:\text{El}(a) \vdash b(x) : \text{U}$ $\Gamma ,a : \text{U} \vdash \sigma (a,b(x)) : \text{U}$ $\Gamma ,a : \text{U} \vdash \alpha : \text{El}(a)$ $\Gamma ,a : \text{U} \vdash \beta : \text{El}(a)$ $\Gamma ,a : \text{U} \vdash \iota (\alpha ,\beta ) : \text{U}$

\[ \]

\[ {\leavevmode \hbox{ \AxiomC {$\Gamma ,a : \text{U}, x:\text{El}(a) \vdash b(x) : \text{U}$} \UnaryInfC {$\Gamma ,a : \text{U} \vdash \text{El}(\pi (a,b(x))) \equiv \prod _{x : \text{El}(a)} \text{El}(b(x)) \text{ type}$} \DisplayProof } \]

$\Gamma ,a : \text{U}, x:\text{El}(a) \vdash b(x) : \text{U}$ $\Gamma ,a : \text{U} \vdash \text{El}(\sigma (a,b(x))) \equiv \sum _{x : \text{El}(a)} \text{El}(b(x)) \text{ type}$

\[ \]

Definitions and Axioms

To simplify, we denote non-dependent products and functions with $\times $ and $\to $. This is not part of the type theory but improves readability.

Truncation Levels

\begin{align*} \text{isContr}(A) & := \sum _{x : A} \prod _{y : A} \text{id}_{A}(y,x)\\ \text{isProp}(A) & := \prod _{x : A} \prod _{y : A} \text{id}_{A}(x,y)\\ \text{isSet}(A) & := \prod _{x : A} \prod _{y: A} \text{isProp}(\text{Id}_{A}(x, y)) \end{align*}

The Set Universe

\[ \text{Set} := \sum _{u : \text{U}} \text{isSet}(\text{El}(u)) \]

Type Equivalence

\[ A \simeq B := \sum _{f :A \to B}\sum _{g :B \to A}\sum _{h :B \to A}\Big(\prod _{a : A} \text{id}_{A}(g(f(a)),a) \Big) \times \Big(\prod _{b : B} \text{id}_{B}(f(h(b)),b) \Big) \]

Set Isomorphism

\[ A \cong B := \text{isSet}(A) \times \text{isSet}(B)\times \sum _{f :A \to B}\sum _{g :B \to A}\Big(\prod _{a : A} \text{id}_{A}(g(f(a)),a) \Big) \times \Big(\prod _{b : B} \text{id}_{B}(f(g(b)),b) \Big) \]

The Univalence Axiom

\[ \text{UA}: \prod _{x : \text{U}} \prod _{y : \text{U}} \text{Id}_{\text{U}}(x,y) \simeq \Big(\text{El}(x) \simeq \text{El}(y)\Big) \]

The Univalence Axiom for Sets

\[ \text{UASet}: \prod _{x : \text{Set}} \prod _{y : \text{Set}} \text{Id}_{\text{Set}}(x,y) \cong \Big(\text{El}(x) \cong \text{El}(y)\Big) \]

Function Extensionality

\[ \text{FunExt}: \prod _{a : \text{U}} \prod _{b : \text{U}} \prod _{f : \text{El}(a) \to \text{El}(b)} \prod _{g : \text{El}(a) \to \text{El}(b)}\Big( \prod _{\alpha : \text{El}(a)}\text{id}_{\text{El(b)}}(f\alpha ,g\alpha )\Big) \simeq \text{id}_{\text{El}(a) \to \text{El}(b)}(f,g) \]