[0024] Internal type theories

A type theory can be internal to another type theory.

Let $T_{1}$ be a type theory and let $T_{2}$ be a type theory internal to $T_{1}$ .

-A construction in $T_{2}$ may have some assumptions from $T_{1}$ .
- $T_{2}$ is an algebraic model of type theory in $T_{1}$ .

We leave it unspecified how the concept of internal type theory is formalized. An algebraic model of type theory is to be something like a contextual category [Cartmell--1978-0000], a category with attributes [Cartmell--1978-0000], or a category with families [Dybjer--1996-0000] but a higher dimensional one. We do not know how to write down its coherence laws.

An internal type theory is more precisely a type theory every small fragment of which is internal to another type theory.

[002C] Notation

Let $T_{1}$ be a type theory and let $T_{2}$ be a type theory internal to $T_{1}$ . We work in $T_{1}$ .

-Let $i:\mathord {\textnormal {\textsf {Level}}}$ . Then $\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i):\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))$ denotes the type of contexts of level $$i$$ in $T_{2}$ . It also denotes the category of contexts of level $$i$$ and morphisms between them.
-Let $i:\mathord {\textnormal {\textsf {Level}}}$ and let $\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i)$ . Then $\mathord {\textnormal {\textsf {D}}}_{T_{2}}(\Gamma \vdash \mathord {\textnormal {\textsf {Type}}}(i)):\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))$ denotes the type of types of level $$i$$ in context $\Gamma$ in $T_{2}$ .
-Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i)$ , and let $A:\mathord {\textnormal {\textsf {D}}}_{T_{2}}(\Gamma \vdash \mathord {\textnormal {\textsf {Type}}}(i))$ . Then $\mathord {\textnormal {\textsf {D}}}_{T_{2}}(\Gamma \vdash A):\mathord {\textnormal {\textsf {Type}}}(i)$ denotes the type of elements of $$A$$ in context $\Gamma$ in $T_{2}$ .

We consider products and coproducts in internal type theories.

[0025] Definition

Let $T_{1}$ be a type theory and let $T_{2}$ be a type theory internal to $T_{1}$ . We work in $T_{2}$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $A:\mathord {\textnormal {\textsf {Type}}}(i)$ in $T_{1}$ , and let $B(x):\mathord {\textnormal {\textsf {Type}}}(i)$ under assumption $$x:A$$ . We say $T_{2}$ has the product of $$B$$ if the following rules are derivable.

- $\prod _{x:A}B(x):\mathord {\textnormal {\textsf {Type}}}(i)$ .
-Let $$b(x):B(x)$$ under assumption $$x:A$$ . Then $x\mapsto b(x):\prod _{x:A}B$ .
-Let $$a:A$$ and let $f:\prod _{x:A}B$ . Then $$f(a):B(a)$$ .
-Let $$a:A$$ and let $$b(x):B(x)$$ under assumption $$x:A$$ . Then $(x\mapsto b(x))(a)\equiv b(a)$ .
-Let $f:\prod _{x:A}B$ . Then $f\equiv x\mapsto f(x)$ .

[0026] Definition

\coprod _{x:A}B(x):\mathord {\textnormal {\textsf {Type}}}(i)

with the following constructors is constructible.

-Let $$a:A$$ and let $$b:B(a)$$ . Then $\mathord {\textnormal {\textsf {in}}}_{a}(b):\coprod _{x:A}B(x)$ .

When a type theory has enough universes, it is a type theory internal to itself.

[002N] Notation

Let $$T$$ be a base type theory. The type theory $$T$$ itself is regarded as a type theory internal to $$T$$ which we call the self-internalization of $$T$$ . Inside $$T$$ , the self-internalization of $$T$$ is referred to as $\mathord {\textnormal {\textsf {Self}}}$ . More precisely, $\mathord {\textnormal {\textsf {Self}}}$ is described as follows. We work in $$T$$ .

-Let $i:\mathord {\textnormal {\textsf {Level}}}$ . Then $\mathord {\textnormal {\textsf {Ctx}}}_{\mathord {\textnormal {\textsf {Self}}}}(i)\equiv \mathcal {U}(i)$ .
-Let $i:\mathord {\textnormal {\textsf {Level}}}$ and let $\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{\mathord {\textnormal {\textsf {Self}}}}(i)$ . Then $\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Self}}}}(\Gamma \vdash \mathord {\textnormal {\textsf {Type}}}(i))\equiv \Gamma \rightarrow \mathcal {U}(i)$ .
-Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{\mathord {\textnormal {\textsf {Self}}}}(i)$ , and let $A:\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Self}}}}(\Gamma \vdash \mathord {\textnormal {\textsf {Type}}}(i))$ . Then $\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Self}}}}(\Gamma \vdash A)\equiv (x:\Gamma )\rightarrow A(x)$ .

We introduce the global section “functor” and its “left adjoint”.

[002P] Definition

Let $T_{1}$ be a base type theory and let $T_{2}$ be a type theory internal to $T_{1}$ . We work in $T_{1}$ . We define a translation

\mathord {\textnormal {\textsf {GS}}}_{T_{2}}:T_{2}\rightarrow \mathord {\textnormal {\textsf {Self}}}

called the global section translation as follows.

-Let $i:\mathord {\textnormal {\textsf {Level}}}$ and let $\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i)$ . Then $\mathord {\textnormal {\textsf {GS}}}_{T_{2}}(\Gamma )\equiv \mathord {\textnormal {\textsf {Hom}}}_{\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i)}(\epsilon ,\Gamma )$ .
-Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i)$ , and let $A:\mathord {\textnormal {\textsf {D}}}_{T_{2}}(\Gamma \vdash \mathord {\textnormal {\textsf {Type}}}(i))$ . Then $\mathord {\textnormal {\textsf {GS}}}_{T_{2}}(A)\equiv x\mapsto \mathord {\textnormal {\textsf {D}}}_{T_{2}}({}\vdash A(x))$ .
-Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $\Gamma :\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(i)$ , let $A:\mathord {\textnormal {\textsf {D}}}_{T_{2}}(\Gamma \vdash \mathord {\textnormal {\textsf {Type}}}(i))$ , and let $a:\mathord {\textnormal {\textsf {D}}}_{T_{2}}(\Gamma \vdash A)$ . Then $\mathord {\textnormal {\textsf {GS}}}_{T_{2}}(a)\equiv x\mapsto a(x)$ .

[002Q] Definition

Let $T_{1}$ be a base type theory and let $T_{2}$ be a type theory internal to $T_{1}$ . We work in $T_{1}$ . Suppose that $T_{2}$ has the unit type and coproducts. Let $i:\mathord {\textnormal {\textsf {Level}}}$ . We define a function

\mathord {\textnormal {\textsf {C}}}_{T_{2}}:\mathcal {U}(i)\rightarrow \mathord {\textnormal {\textsf {D}}}_{T_{2}}({}\vdash \mathord {\textnormal {\textsf {Type}}}(i))

\mathord {\textnormal {\textsf {C}}}_{T_{2}}(A)\equiv \coprod _{\_:A}\mathord {\textnormal {\textsf {1}}}

[002R] Exercise

Let $T_{1}$ be a base type theory and let $T_{2}$ be a type theory internal to $T_{1}$ . We work in $T_{1}$ . Suppose that $T_{2}$ has the unit type and coproducts. Then $\mathord {\textnormal {\textsf {C}}}_{T_{2}}$ is a “left adjoint” of $\mathord {\textnormal {\textsf {GS}}}_{T_{2}}$ .

[002T] Notation

Let $T_{1}$ be a base type theory, let $T_{2}$ be a type theory internal to $T_{1}$ , and let $T_{3}$ be a type theory internal to $T_{2}$ . We work in $T_{1}$ . Since the translation $\mathord {\textnormal {\textsf {GS}}}_{T_{2}}:T_{2}\rightarrow \mathord {\textnormal {\textsf {Self}}}$ is a right adjoint, it preserves arbitrary algebraic structures. In particular, it takes $T_{3}$ to a type theory internal to $T_{1}$ which we refer to as $\mathord {\textnormal {\textsf {Glob}}}_{T_{2}}(T_{3})$ and call the globalization of $T_{3}$ .

[004F] Terminology

Let $T_{1}$ be a type theory and let $T_{2}$ be a type theory internal to $T_{1}$ . We work in $T_{1}$ . When we mention an object in $T_{2}$ , the object is understood in the empty context in $T_{2}$ . For example, “let $A:\mathord {\textnormal {\textsf {Type}}}(i)$ in $T_{2}$ ” means “let $A:\mathord {\textnormal {\textsf {D}}}_{T_{2}}({}\vdash \mathord {\textnormal {\textsf {Type}}}(i))$ ”.