[[!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. ### Application of a family of elements across an identification $$\mathrm{ap}_{x:A.B(x)}^{x:A.f(x)}(a, b, p):\mathrm{ind}_{\Pi x:A.B(x)}(\mathrm{transport}_{x:A.B(x)}(a, b, p), f(a)) =_{B(b)} f(b)$$ inductively defined by $$\mathrm{ap}_{x:A.B(x)}^{x:A.f(x)}(a, a, \mathrm{refl}_A(a)) \equiv \beta_{\Pi x:A.B(x)}^{x:A.\mathrm{transport}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a))(x)}:\mathrm{ind}_{\Pi x:A.B(x)}(\mathrm{transport}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a)), f(a)) =_{B(a)} f(a)$$ and non-dependent application $$\mathrm{ap}_{B}^{x:A.f(x)}(a, b, p):\mathrm{transport}_{B}(a, b, p, f(a)) =_{B} f(b)$$ inductively defined by $$\mathrm{ap}_{B}^{x:A.f(x)}(a, a, \mathrm{refl}_A(a)) \equiv \mathrm{refl}_A(a):\mathrm{transport}_{B}(a, a, \mathrm{refl}_A(a), f(a)) =_{B} f(a)$$ ### Equivalences Equivalences between types $A$ and $B$ consist of a type family $x:A \vdash f(x):B$, a type family $y:B \vdash f^{-1}(y):A$, a family of identifications $y:B \vdash \mathrm{sec}_f(y):f(f^{-1}(y)) =_B y$, a family of identifications $$y:B, x:A, p:f(x) =_B y \vdash \mathrm{adj}_f(y, x, p):f^{-1}(y) =_A x$$ and a family of identifications $$y:B, x:A, p:f(x) =_B y \vdash \mathrm{coh}_f(y, x, p):\mathrm{transport}_{x:A.f(x) =_B y}(f^{-1}(y), x, \mathrm{adj}_f(y, x, p), \mathrm{sec}_f(y)) =_{f(x) =_B y} p$$ To get the retraction $x:A \vdash f^{-1}(f(x)) =_A x$ we apply the type family $x:A \vdash f(x):B$ across the identification $\mathrm{adj}_f(y, x, p):f^{-1}(y) =_A x$ $$y:B, x:A, p:f(x) =_B y \vdash \mathrm{adj}_f(y, x, p):f^{-1}(y) =_A x$$ category: redirected to nlab