[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] ### Without a separate type judgment In this section, we describe a formalization of objective type theory using an infinite hierarchy of Russell universes with cumulativity. #### Judgments, contexts, and universes This presentation of objective type theory consists of the following judgments: * Element judgments, where we judge $a$ to be an element of $A$, $a:A$ * Context judgments, where we judge $\Gamma$ to be a context, $\Gamma \; \mathrm{ctx}$. In addition, we have a [[countable set|countably]] [[infinite set|infinite]] number of [[inference rules]] for the countably infinite number of [[Russell universes]] $\mathrm{Type}_0, \mathrm{Type}_1, \mathrm{Type}_2, \ldots$ in the theory, here represented by a [[natural numbers]] [[metavariable]] for conciseness: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Type}_i:\mathrm{Type}_{i + 1}}$$ as well as inference rules for [[cumulativity]], that any type in a universe is also in the next universe of the hierarchy: $$\frac{\Gamma \vdash A:\mathrm{Type}_i}{\Gamma \vdash A:\mathrm{Type}_{i + 1}}\mathrm{cumul}$$ Contexts are lists of element judgments $a:A$, $b:B$, $c:C$, et cetera, and are formalized by the inference rules for the empty context and extending the context by a element judgment $$\frac{}{() \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A:\mathrm{Type}_i}{(\Gamma, a:A) \; \mathrm{ctx}}$$ #### Variable rule There is one additional [[structural rule]] in objective type theory, the [[variable rule]]. The variable rule states that we may derive a element judgment if the element judgment is in the context already: $$\frac{\Gamma, a:A, \Delta \; \mathrm{ctx}}{\Gamma, a:A, \Delta \vdash a:A}$$ #### Admissible structural rules The [[weakening rule]] and the [[substitution rule]] 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. Let $\mathcal{J}$ be any arbitrary judgment. Then the weakening rule is $$\frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash A:\mathrm{Type}_i}{\Gamma, a:A, \Delta \vdash \mathcal{J}}$$ and the substitution rule is $$\frac{\Gamma \vdash a:A \quad \Gamma, b:A, \Delta(b) \vdash \mathcal{J}(b)}{\Gamma, \Delta(a) \vdash \mathcal{J}(a)}$$ #### Families of types and elements A family of elements is an element $b:B$ in the context of the variable judgment $x:A$, $x:A \vdash b:B$. They are usually written as $b(x)$ to indicate its dependence upon $x$. Given a particular element $a:A$, the element $b(a)$ is an element dependent upon $a:A$. Since types are elements of universe, a family of types is simply a family of elements of universes. #### Basic type formers Formation rules for function types: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, A:\mathrm{Type}_i, B:\mathrm{Type}_i \vdash A \to B:\mathrm{Type}_i}$$ Formation rules for dependent function types: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, A:\mathrm{Type}_i, B:A \to \mathrm{Type}_i \vdash \Pi(A, B):\mathrm{Type}_i}$$ Formation rules for identification types: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, A:\mathrm{Type}_i, a:A, b:A \vdash \mathrm{Id}(A, a, b):\mathrm{Type}_i}$$ Introduction rules for function types: $$\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i \quad \Gamma, x:A \vdash b(x):B}{\Gamma \vdash \lambda(x:A).b(x):A \to B}$$ Introduction rules for identification types: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, A:\mathrm{Type}_i, a:A \vdash \mathrm{refl}(A, a):\mathrm{Id}(A, a, a)}$$ Elimination rules for function types: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, A:\mathrm{Type}_i, B:\mathrm{Type}_i, f:A \to B, a:A \vdash \mathrm{ind}_\mathrm{Func}(A, B, f, a):B}$$ Introduction rules for dependent function types: $$\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:A \to \mathrm{Type}_i \quad \Gamma, x:A \vdash b(x):\mathrm{ind}_\mathrm{Func}(A, \mathrm{Type}_i, B, x)}{\Gamma \vdash \lambda(x:A).b(x):\Pi(A, B)}$$ Elimination rules for dependent function types: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, A:\mathrm{Type}_i, B:A \to \mathrm{Type}_i, f:\Pi(A, B), a:A \vdash \mathrm{ind}_{\Pi}(A, B, f, a):\mathrm{ind}_\mathrm{Func}(A, \mathrm{Type}_i, B, a)}$$ Elimination rule for identification types: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, A:\mathrm{Type}_i, C:\prod_{x:A} \prod_{y:A} \mathrm{Id}(A, x, y) \to \mathrm{Type}_i \vdash \mathrm{ind}_{\mathrm{Id}}(A, C):\left(\prod_{x:A} C(x, x, \mathrm{refl}(A, x)\right) \to \left(\prod_{x:A} \prod_{y:A} \prod_{p:\mathrm{Id}(A, x, y)} C(x, y, p)\right)}$$ Computation rules for function types $$\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i \quad \Gamma, x:A \vdash b(x):B}{\Gamma \vdash \beta_\mathrm{Func}^{A, B} (x:A).b(x):\Pi(A, \lambda (a:A).\mathrm{Id}(B, \mathrm{ind}_\mathrm{Func}(A, B, \lambda(x:A).b(x), a), b(a))}$$ Computation rules for identification types: $$\frac{\Gamma, x:A, y:A, p:x =_A y, \Delta(x, y, p) \vdash C(x, y, p):\mathrm{Type}_i \quad \Gamma, x:A, \Delta(x, x, \mathrm{refl}_A(x)) \vdash t(x):C(x, x, \mathrm{refl}_A(x))}{\Gamma, x:A, \Delta(x, x, \mathrm{refl}_A(x)) \vdash \beta_{=_A}^{x:A.t(x)}(x):\mathrm{ind}_{=_A}^{x:A.t(x)}(x, x, \mathrm{refl}_A(x)) =_{C(x, x, \mathrm{refl}_A(x))} t(x)}$$ Computation rules for dependent function types $$\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i \quad \Gamma, x:A \vdash b(x):B(x)}{\Gamma, a:A \vdash \beta_{\prod_{x:A} B(x)}(a):\mathrm{ind}_{\prod_{x:A} B(x)}(\lambda(x:A).b(x), a) =_{B(a)} b(a)}$$ Uniqueness rules for dependent function types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x):\mathrm{Type}_i}{\Gamma, f:\prod_{x:A} B(x) \vdash \eta_{\prod_{x:A} B(x)}(f):f =_{\prod_{x:A} B(x)} \lambda(x:A).\mathrm{ind}_{\prod_{x:A} B(x)}(f, x)}$$ Uniqueness rules for function types: $$\frac{\Gamma \vdash A:\mathrm{Type}_i \quad \Gamma \vdash B:\mathrm{Type}_i}{\Gamma, f:A \to B \vdash \eta_{A \to B}(f):f =_{A \to B} \lambda(x:A).\mathrm{ind}_{A \to B}(f, x)}$$ category: redirected to nlab